set X = { v where v is Element of F1() : ( P1[v] or P2[v] ) } ;
set Y = { v1 where v1 is Element of F1() : P1[v1] } ;
set Z = { v2 where v2 is Element of F1() : P2[v2] } ;
now :: thesis: for x being object holds
( ( for x being object st x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } holds
x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } ) & ( x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } implies x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } ) )
let x be object ; :: thesis: ( ( for x being object st x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } holds
x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } ) & ( x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } implies b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) } ) )
thus for x being object st x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } holds
x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } :: thesis: ( x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } implies b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) } )
proof
let x be object ; :: thesis: ( x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } implies x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } )
assume x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } ; :: thesis: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] }
then consider v being Element of F1() such that
A1: x = v and
A2: ( P1[v] or P2[v] ) ;
per cases ( P1[v] or P2[v] ) by A2;
suppose P1[v] ; :: thesis: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] }
then x in { v1 where v1 is Element of F1() : P1[v1] } by A1;
hence x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } by XBOOLE_0:def 3; :: thesis: verum
end;
suppose P2[v] ; :: thesis: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] }
then x in { v2 where v2 is Element of F1() : P2[v2] } by A1;
hence x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
assume A3: x in { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } ; :: thesis: b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) }
per cases ( x in { v1 where v1 is Element of F1() : P1[v1] } or x in { v2 where v2 is Element of F1() : P2[v2] } ) by A3, XBOOLE_0:def 3;
suppose x in { v1 where v1 is Element of F1() : P1[v1] } ; :: thesis: b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) }
then ex v being Element of F1() st
( x = v & P1[v] ) ;
hence x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } ; :: thesis: verum
end;
suppose x in { v2 where v2 is Element of F1() : P2[v2] } ; :: thesis: b1 in { b2 where v is Element of F1() : ( P1[b2] or P2[b2] ) }
then ex v being Element of F1() st
( x = v & P2[v] ) ;
hence x in { v where v is Element of F1() : ( P1[v] or P2[v] ) } ; :: thesis: verum
end;
end;
end;
hence { v where v is Element of F1() : ( P1[v] or P2[v] ) } = { v1 where v1 is Element of F1() : P1[v1] } \/ { v2 where v2 is Element of F1() : P2[v2] } by TARSKI:2; :: thesis: verum