let x, y be object ; :: thesis: for Y being set st not y in union Y holds
card Y = card (Ext (Y,x,y))
let Y be set ; :: thesis: ( not y in union Y implies card Y = card (Ext (Y,x,y)) )
assume A1: not y in union Y ; :: thesis: card Y = card (Ext (Y,x,y))
set P = { X where X is Element of Y : x in X } ;
set Py = { (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 ) } ;
deffunc H₁( set ) -> set = $1 \/ {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 \/ {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 \/ {y}) where X is Element of Y : x in X } )
assume a in rng f ; :: thesis: a in { (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 \/ {y} & ex X being Element of Y st
( b = X & x in X ) ) by A4, A2;
hence a in { (X \/ {y}) where X is Element of Y : x in X } ; :: thesis: verum

end;

{ (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 \/ {y}) where X is Element of Y : x in X } or a in rng f )
assume a in { (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 \/ {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 \/ {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 \/ {y} & f . b = b \/ {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 ) by A10, ZFMISC_1:74;
then ( {y} misses a & {y} misses b ) by A1, ZFMISC_1:50;
hence a = b by A8, A9, XBOOLE_1:71; :: thesis: verum

end;

then A11: { X where X is Element of Y : x in X } , { (X \/ {y}) where X is Element of Y : x in X } are_equipotent by A2, A7, WELLORD2:def 4;
A12: { 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 A13: ex X being Element of Y st
( a = X & x in X ) ;
then Y <> {} by SUBSET_1:def 1;
hence a in Y by A13; :: thesis: verum

end;

A14: { 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 A15: 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 A15;
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 A16: 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 A12, A14, XBOOLE_1:8;
A17: { X where X is Element of Y : ( not x in X & X in Y ) } misses { (X \/ {y}) 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 \/ {y}) where X is Element of Y : x in X } ; :: thesis: contradiction
then consider a being object such that
A18: a in { X where X is Element of Y : ( not x in X & X in Y ) } /\ { (X \/ {y}) 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 A18, XBOOLE_0:def 4;
then consider A being Element of Y such that
A19: ( a = A & not x in A & A in Y ) ;
a in { (X \/ {y}) where X is Element of Y : x in X } by A18, XBOOLE_0:def 4;
then ex B being Element of Y st
( a = B \/ {y} & x in B ) ;
hence contradiction by A19, XBOOLE_0:def 3; :: 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
A20: 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 A20, XBOOLE_0:def 4;
then consider A being Element of Y such that
A21: ( a = A & not x in A & A in Y ) ;
a in { X where X is Element of Y : x in X } by A20, XBOOLE_0:def 4;
then ex B being Element of Y st
( a = B & x in B ) ;
hence contradiction by A21; :: thesis: verum

end;

hence card Y = card (Ext (Y,x,y)) by CARD_1:5, A17, A11, CARD_1:31, A16; :: thesis: verum