let x, y be object ; :: thesis: for Y being set st not y in union Y holds
card Y = card (swap (Y,x,y))
let Y be set ; :: thesis: ( not y in union Y implies card Y = card (swap (Y,x,y)) )
assume A1: not y in union Y ; :: thesis: card Y = card (swap (Y,x,y))
set P = { X where X is Element of Y : x in X } ;
set Py = { ((X \ {x}) \/ {y}) where X is Element of Y : x in X } ;
set N = { X where X is Element of Y : ( not x in X & X in Y ) } ;
set Nx = { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } ;
deffunc H₁( set ) -> set = ($1 \ {x}) \/ {y};
consider f being Function such that
A2: ( dom f = { X where X is Element of Y : x in X } & ( for A being set st A in { X where X is Element of Y : x in X } holds
f . A = H₁(A) ) ) from FUNCT_1:sch 5();
A3: rng f c= { ((X \ {x}) \/ {y}) where X is Element of Y : x in X }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in { ((X \ {x}) \/ {y}) where X is Element of Y : x in X } )
assume a in rng f ; :: thesis: a in { ((X \ {x}) \/ {y}) where X is Element of Y : x in X }
then consider b being object such that
A4: ( b in dom f & f . b = a ) by FUNCT_1:def 3;
reconsider b = b as set by TARSKI:1;
( a = (b \ {x}) \/ {y} & ex X being Element of Y st
( b = X & x in X ) ) by A4, A2;
hence a in { ((X \ {x}) \/ {y}) where X is Element of Y : x in X } ; :: thesis: verum

end;

{ ((X \ {x}) \/ {y}) where X is Element of Y : x in X } c= rng f

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { ((X \ {x}) \/ {y}) where X is Element of Y : x in X } or a in rng f )
assume a in { ((X \ {x}) \/ {y}) where X is Element of Y : x in X } ; :: thesis: a in rng f
then consider X being Element of Y such that
A5: ( a = (X \ {x}) \/ {y} & x in X ) ;
A6: X in { X where X is Element of Y : x in X } by A5;
then f . X = a by A5, A2;
hence a in rng f by A2, A6, FUNCT_1:def 3; :: thesis: verum

end;

then A7: rng f = { ((X \ {x}) \/ {y}) where X is Element of Y : x in X } by A3;
f is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom f or not b in dom f or not f . a = f . b or a = b )
assume A8: ( a in dom f & b in dom f & f . a = f . b ) ; :: thesis: a = b
reconsider a = a, b = b as set by TARSKI:1;
A9: ( f . a = (a \ {x}) \/ {y} & f . b = (b \ {x}) \/ {y} ) by A2, A8;
A10: ( ex X being Element of Y st
( a = X & x in X ) & ex X being Element of Y st
( b = X & x in X ) ) by A8, A2;
then Y <> {} by SUBSET_1:def 1;
then ( a c= union Y & b c= union Y & x in a & x in b ) by A10, ZFMISC_1:74;
then ( {y} misses a & {y} misses b ) by A1, ZFMISC_1:50;
then ( {y} misses a \ {x} & {y} misses b \ {x} ) by XBOOLE_1:80;
then a \ {x} = b \ {x} by A8, A9, XBOOLE_1:71;
then ( a = (a \ {x}) \/ {x} & (a \ {x}) \/ {x} = b ) by ZFMISC_1:116, A10;
hence a = b ; :: thesis: verum

end;

then A11: { X where X is Element of Y : x in X } , { ((X \ {x}) \/ {y}) where X is Element of Y : x in X } are_equipotent by A2, A7, WELLORD2:def 4;
deffunc H₂( set ) -> set = $1 \/ {x};
consider g being Function such that
A12: ( dom g = { X where X is Element of Y : ( not x in X & X in Y ) } & ( for A being set st A in { X where X is Element of Y : ( not x in X & X in Y ) } holds
g . A = H₂(A) ) ) from FUNCT_1:sch 5();
A13: rng g c= { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng g or a in { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } )
assume a in rng g ; :: thesis: a in { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) }
then consider b being object such that
A14: ( b in dom g & g . b = a ) by FUNCT_1:def 3;
reconsider b = b as set by TARSKI:1;
( a = b \/ {x} & ex X being Element of Y st
( b = X & not x in X & X in Y ) ) by A14, A12;
hence a in { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } ; :: thesis: verum

end;

{ (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } c= rng g

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } or a in rng g )
assume a in { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } ; :: thesis: a in rng g
then consider X being Element of Y such that
A15: ( a = X \/ {x} & not x in X & X in Y ) ;
A16: X in { X where X is Element of Y : ( not x in X & X in Y ) } by A15;
then g . X = a by A15, A12;
hence a in rng g by A12, A16, FUNCT_1:def 3; :: thesis: verum

end;

then A17: rng g = { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } by A13;
g is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom g or not b in dom g or not g . a = g . b or a = b )
assume A18: ( a in dom g & b in dom g & g . a = g . b ) ; :: thesis: a = b
reconsider a = a, b = b as set by TARSKI:1;
A19: ( g . a = a \/ {x} & g . b = b \/ {x} ) by A12, A18;
( ex X being Element of Y st
( a = X & not x in X & X in Y ) & ex X being Element of Y st
( b = X & not x in X & X in Y ) ) by A18, A12;
then ( {x} misses a & {x} misses b ) by ZFMISC_1:50;
hence a = b by A18, A19, XBOOLE_1:71; :: thesis: verum

end;

then A20: { X where X is Element of Y : ( not x in X & X in Y ) } , { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } are_equipotent by A12, A17, WELLORD2:def 4;
A21: { X where X is Element of Y : x in X } c= Y

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { X where X is Element of Y : x in X } or a in Y )
assume a in { X where X is Element of Y : x in X } ; :: thesis: a in Y
then A22: ex X being Element of Y st
( a = X & x in X ) ;
then Y <> {} by SUBSET_1:def 1;
hence a in Y by A22; :: thesis: verum

end;

A23: { X where X is Element of Y : ( not x in X & X in Y ) } c= Y

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { X where X is Element of Y : ( not x in X & X in Y ) } or a in Y )
assume a in { X where X is Element of Y : ( not x in X & X in Y ) } ; :: thesis: a in Y
then ex X being Element of Y st
( a = X & not x in X & X in Y ) ;
hence a in Y ; :: thesis: verum

end;

Y c= { X where X is Element of Y : ( not x in X & X in Y ) } \/ { X where X is Element of Y : x in X }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Y or a in { X where X is Element of Y : ( not x in X & X in Y ) } \/ { X where X is Element of Y : x in X } )
assume A24: a in Y ; :: thesis: a in { X where X is Element of Y : ( not x in X & X in Y ) } \/ { X where X is Element of Y : x in X }
then reconsider a = a as Element of Y ;
( x in a or not x in a ) ;
then ( a in { X where X is Element of Y : x in X } or a in { X where X is Element of Y : ( not x in X & X in Y ) } ) by A24;
hence a in { X where X is Element of Y : ( not x in X & X in Y ) } \/ { X where X is Element of Y : x in X } by XBOOLE_0:def 3; :: thesis: verum

end;

then A25: Y = { X where X is Element of Y : ( not x in X & X in Y ) } \/ { X where X is Element of Y : x in X } by A21, A23, XBOOLE_1:8;
A26: { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } misses { ((X \ {x}) \/ {y}) where X is Element of Y : x in X }

proof

assume { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } meets { ((X \ {x}) \/ {y}) where X is Element of Y : x in X } ; :: thesis: contradiction
then consider a being object such that
A27: a in { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } /\ { ((X \ {x}) \/ {y}) where X is Element of Y : x in X } by XBOOLE_0:4;
a in { (X \/ {x}) where X is Element of Y : ( not x in X & X in Y ) } by A27, XBOOLE_0:def 4;
then consider A being Element of Y such that
A28: ( a = A \/ {x} & not x in A & A in Y ) ;
a in { ((X \ {x}) \/ {y}) where X is Element of Y : x in X } by A27, XBOOLE_0:def 4;
then consider B being Element of Y such that
A29: ( a = (B \ {x}) \/ {y} & x in B ) ;
A30: x in union Y by A28, A29, TARSKI:def 4;
x in {x} by TARSKI:def 1;
then x in (B \ {x}) \/ {y} by A28, A29, XBOOLE_0:def 3;
then ( x in B \ {x} or x in {y} ) by XBOOLE_0:def 3;
hence contradiction by ZFMISC_1:56, TARSKI:def 1, A30, A1; :: thesis: verum

end;

{ X where X is Element of Y : ( not x in X & X in Y ) } misses { X where X is Element of Y : x in X }

proof

assume { X where X is Element of Y : ( not x in X & X in Y ) } meets { X where X is Element of Y : x in X } ; :: thesis: contradiction
then consider a being object such that
A31: a in { X where X is Element of Y : ( not x in X & X in Y ) } /\ { X where X is Element of Y : x in X } by XBOOLE_0:4;
a in { X where X is Element of Y : ( not x in X & X in Y ) } by A31, XBOOLE_0:def 4;
then consider A being Element of Y such that
A32: ( a = A & not x in A & A in Y ) ;
a in { X where X is Element of Y : x in X } by A31, XBOOLE_0:def 4;
then ex B being Element of Y st
( a = B & x in B ) ;
hence contradiction by A32; :: thesis: verum

end;

hence card Y = card (swap (Y,x,y)) by CARD_1:5, A26, A11, A20, CARD_1:31, A25; :: thesis: verum