set D = { d where d is Element of F2() : F3(d) in F1() } ;
per cases
( F1() = {} or F1() <> {} )
;
suppose
F1()
<> {}
;
F1(), { d where d is Element of F2() : F3(d) in F1() } are_equipotent then reconsider A =
F1() as non
empty set ;
A,
{ d where d is Element of F2() : F3(d) in F1() } are_equipotent
proof
take Z =
{ [F3(d),d] where d is Element of F2() : verum } ;
TARSKI:def 6 ( ( for b1 being object holds
( not b1 in A or ex b2 being object st
( b2 in { d where d is Element of F2() : F3(d) in F1() } & [b1,b2] in Z ) ) ) & ( for b1 being object holds
( not b1 in { d where d is Element of F2() : F3(d) in F1() } or ex b2 being object st
( b2 in A & [b2,b1] in Z ) ) ) & ( for b1, b2, b3, b4 being object holds
( not [b1,b2] in Z or not [b3,b4] in Z or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
hereby ( ( for b1 being object holds
( not b1 in { d where d is Element of F2() : F3(d) in F1() } or ex b2 being object st
( b2 in A & [b2,b1] in Z ) ) ) & ( for b1, b2, b3, b4 being object holds
( not [b1,b2] in Z or not [b3,b4] in Z or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
end;
hereby for b1, b2, b3, b4 being object holds
( not [b1,b2] in Z or not [b3,b4] in Z or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) )
let y be
object ;
( y in { d where d is Element of F2() : F3(d) in F1() } implies ex x being object st
( x in A & [x,y] in Z ) )assume
y in { d where d is Element of F2() : F3(d) in F1() }
;
ex x being object st
( x in A & [x,y] in Z )then consider d being
Element of
F2()
such that A6:
(
d = y &
F3(
d)
in A )
;
reconsider x =
F3(
d) as
object ;
take x =
x;
( x in A & [x,y] in Z )thus
(
x in A &
[x,y] in Z )
by A6;
verum
end;
let x,
y,
z,
u be
object ;
( 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
;
( not [z,u] in Z or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
then consider d1 being
Element of
F2()
such that A7:
[x,y] = [F3(d1),d1]
;
assume
[z,u] in Z
;
( ( not x = z or y = u ) & ( not y = u or x = z ) )
then consider d2 being
Element of
F2()
such that A8:
[z,u] = [F3(d2),d2]
;
A9:
(
z = F3(
d2) &
u = d2 )
by A8, XTUPLE_0:1;
(
x = F3(
d1) &
y = d1 )
by A7, XTUPLE_0:1;
hence
( ( not
x = z or
y = u ) & ( not
y = u or
x = z ) )
by A2, A9;
verum
end; hence
F1(),
{ d where d is Element of F2() : F3(d) in F1() } are_equipotent
;
verum end; end;