A1:
X . v, FreeGen (v,X) are_equipotent
proof
set Z =
{ [a,(root-tree [a,v])] where a is Element of X . v : verum } ;
take
{ [a,(root-tree [a,v])] where a is Element of X . v : verum }
;
TARSKI:def 6 ( ( for b1 being set holds
( not b1 in X . v or ex b2 being set st
( b2 in FreeGen (v,X) & [b1,b2] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) ) ) & ( for b1 being set holds
( not b1 in FreeGen (v,X) or ex b2 being set st
( b2 in X . v & [b2,b1] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [b3,b4] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
hereby ( ( for b1 being set holds
( not b1 in FreeGen (v,X) or ex b2 being set st
( b2 in X . v & [b2,b1] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) ) ) & ( for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [b3,b4] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) ) ) )
let x be
set ;
( x in X . v implies ex y being set st
( y in FreeGen (v,X) & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) )assume A2:
x in X . v
;
ex y being set st
( y in FreeGen (v,X) & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } )reconsider y =
root-tree [x,v] as
set ;
take y =
y;
( y in FreeGen (v,X) & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } )thus
y in FreeGen (
v,
X)
by A2, MSAFREE:def 17;
[x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } thus
[x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum }
by A2;
verum
end;
hereby for b1, b2, b3, b4 being set holds
( not [b1,b2] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [b3,b4] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not b1 = b3 or b2 = b4 ) & ( not b2 = b4 or b1 = b3 ) ) )
let y be
set ;
( y in FreeGen (v,X) implies ex x being set st
( x in X . v & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) )assume
y in FreeGen (
v,
X)
;
ex x being set st
( x in X . v & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } )then consider x being
set such that A3:
x in X . v
and A4:
y = root-tree [x,v]
by MSAFREE:def 17;
take x =
x;
( x in X . v & [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } )thus
x in X . v
by A3;
[x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } thus
[x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum }
by A3, A4;
verum
end;
let x,
y,
z,
u be
set ;
( not [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [z,u] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not x = z or y = u ) & ( not y = u or x = z ) ) )
assume that A5:
[x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum }
and A6:
[z,u] in { [a,(root-tree [a,v])] where a is Element of X . v : verum }
;
( ( not x = z or y = u ) & ( not y = u or x = z ) )
consider a being
Element of
X . v such that A7:
[x,y] = [a,(root-tree [a,v])]
by A5;
consider b being
Element of
X . v such that A8:
[z,u] = [b,(root-tree [b,v])]
by A6;
A9:
z = b
by A8, ZFMISC_1:33;
A10:
x = a
by A7, ZFMISC_1:33;
hence
(
x = z implies
y = u )
by A7, A8, A9, ZFMISC_1:33;
( not y = u or x = z )
A11:
y = root-tree [a,v]
by A7, ZFMISC_1:33;
A12:
u = root-tree [b,v]
by A8, ZFMISC_1:33;
assume
y = u
;
x = z
then
[a,v] = [b,v]
by A11, A12, TREES_4:4;
hence
x = z
by A10, A9, ZFMISC_1:33;
verum
end;
X . v is finite
by FINSET_1:def 4;
hence
FreeGen (v,X) is finite
by A1, CARD_1:68; verum