set D = { d where d is Element of F₂() : F₃(d) in F₁() } ;

per cases ( F₁() = {} or F₁() <> {} ) ;

suppose A3: F₁() = {} ; :: thesis: F₁(), { d where d is Element of F₂() : F₃(d) in F₁() } are_equipotent

now :: thesis: not { d where d is Element of F₂() : F₃(d) in F₁() } <> {}

set a = the Element of { d where d is Element of F₂() : F₃(d) in F₁() } ;
assume { d where d is Element of F₂() : F₃(d) in F₁() } <> {} ; :: thesis: contradiction
then the Element of { d where d is Element of F₂() : F₃(d) in F₁() } in { d where d is Element of F₂() : F₃(d) in F₁() } ;
then ex d being Element of F₂() st
( the Element of { d where d is Element of F₂() : F₃(d) in F₁() } = d & F₃(d) in F₁() ) ;
hence contradiction by A3; :: thesis: verum

end;

hence F₁(), { d where d is Element of F₂() : F₃(d) in F₁() } are_equipotent by A3; :: thesis: verum

end;

suppose F₁() <> {} ; :: thesis: F₁(), { d where d is Element of F₂() : F₃(d) in F₁() } are_equipotent

then reconsider A = F₁() as non empty set ;
A, { d where d is Element of F₂() : F₃(d) in F₁() } are_equipotent

proof

take Z = { [F₃(d),d] where d is Element of F₂() : verum } ; :: according to TARSKI:def 6 :: thesis: ( ( for b₁ being object holds
( not b₁ in A or ex b₂ being object st
( b₂ in { d where d is Element of F₂() : F₃(d) in F₁() } & [b₁,b₂] in Z ) ) ) & ( for b₁ being object holds
( not b₁ in { d where d is Element of F₂() : F₃(d) in F₁() } or ex b₂ being object st
( b₂ in A & [b₂,b₁] in Z ) ) ) & ( for b₁, b₂, b₃, b₄ being object holds
( not [b₁,b₂] in Z or not [b₃,b₄] in Z or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )

hereby :: thesis: ( ( for b₁ being object holds
( not b₁ in { d where d is Element of F₂() : F₃(d) in F₁() } or ex b₂ being object st
( b₂ in A & [b₂,b₁] in Z ) ) ) & ( for b₁, b₂, b₃, b₄ being object holds
( not [b₁,b₂] in Z or not [b₃,b₄] in Z or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )

let x be object ; :: thesis: ( x in A implies ex d being object st
( d in { d where d is Element of F₂() : F₃(d) in F₁() } & [x,d] in Z ) )
assume A4: x in A ; :: thesis: ex d being object st
( d in { d where d is Element of F₂() : F₃(d) in F₁() } & [x,d] in Z )
then consider d being Element of F₂() such that
A5: x = F₃(d) by A1;
reconsider d = d as object ;
take d = d; :: thesis: ( d in { d where d is Element of F₂() : F₃(d) in F₁() } & [x,d] in Z )
thus d in { d where d is Element of F₂() : F₃(d) in F₁() } by A4, A5; :: thesis: [x,d] in Z
thus [x,d] in Z by A5; :: thesis: verum

end;

hereby :: thesis: for b₁, b₂, b₃, b₄ being object holds
( not [b₁,b₂] in Z or not [b₃,b₄] in Z or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) )

let y be object ; :: thesis: ( y in { d where d is Element of F₂() : F₃(d) in F₁() } implies ex x being object st
( x in A & [x,y] in Z ) )
assume y in { d where d is Element of F₂() : F₃(d) in F₁() } ; :: thesis: ex x being object st
( x in A & [x,y] in Z )
then consider d being Element of F₂() such that
A6: ( d = y & F₃(d) in A ) ;
reconsider x = F₃(d) as object ;
take x = x; :: thesis: ( x in A & [x,y] in Z )
thus ( x in A & [x,y] in Z ) by A6; :: thesis: verum

end;

let x, y, z, u be object ; :: thesis: ( not [x,y] in Z or not [z,u] in Z or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
assume [x,y] in Z ; :: thesis: ( not [z,u] in Z or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
then consider d1 being Element of F₂() such that
A7: [x,y] = [F₃(d1),d1] ;
assume [z,u] in Z ; :: thesis: ( ( not x = z or y = u ) & ( not y = u or x = z ) )
then consider d2 being Element of F₂() such that
A8: [z,u] = [F₃(d2),d2] ;
A9: ( z = F₃(d2) & u = d2 ) by A8, XTUPLE_0:1;
( x = F₃(d1) & y = d1 ) by A7, XTUPLE_0:1;
hence ( ( not x = z or y = u ) & ( not y = u or x = z ) ) by A2, A9; :: thesis: verum

end;

hence F₁(), { d where d is Element of F₂() : F₃(d) in F₁() } are_equipotent ; :: thesis: verum

end;

end;