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 } ; :: according to TARSKI:def 6 :: thesis: ( ( for b₁ being set holds
( not b₁ in X . v or ex b₂ being set st
( b₂ in FreeGen v,X & [b₁,b₂] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) ) ) & ( for b₁ being set holds
( not b₁ in FreeGen v,X or ex b₂ being set st
( b₂ in X . v & [b₂,b₁] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) ) ) & ( for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [b₃,b₄] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )

hereby :: thesis: ( ( for b₁ being set holds
( not b₁ in FreeGen v,X or ex b₂ being set st
( b₂ in X . v & [b₂,b₁] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) ) ) & ( for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [b₃,b₄] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )

let x be set ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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; :: thesis: [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; :: thesis: verum

end;

hereby :: thesis: for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or not [b₃,b₄] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) )

let y be set ; :: thesis: ( 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 ; :: thesis: 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 & y = root-tree [x,v] ) by MSAFREE:def 17;
take x = x; :: thesis: ( 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; :: thesis: [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; :: thesis: verum

end;

let x, y, z, u be set ; :: thesis: ( 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 A4: ( [x,y] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } & [z,u] in { [a,(root-tree [a,v])] where a is Element of X . v : verum } ) ; :: thesis: ( ( not x = z or y = u ) & ( not y = u or x = z ) )
then consider a being Element of X . v such that
A5: [x,y] = [a,(root-tree [a,v])] ;
consider b being Element of X . v such that
A6: [z,u] = [b,(root-tree [b,v])] by A4;
A7: ( x = a & y = root-tree [a,v] & z = b & u = root-tree [b,v] ) by A5, A6, ZFMISC_1:33;
hence ( x = z implies y = u ) ; :: thesis: ( not y = u or x = z )
assume y = u ; :: thesis: x = z
then [a,v] = [b,v] by A7, TREES_4:4;
hence x = z by A7, ZFMISC_1:33; :: thesis: verum

end;

X . v is finite by FINSET_1:def 4;
hence FreeGen v,X is finite by A1, CARD_1:68; :: thesis: verum