set X = { F4(j) where j is Element of F1() : j in {F2(),F3()} } ;
for x being object holds
( x in F4(F2()) \/ F4(F3()) iff ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ) )
proof
let x be object ; :: thesis: ( x in F4(F2()) \/ F4(F3()) iff ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ) )
thus ( x in F4(F2()) \/ F4(F3()) implies ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ) ) :: thesis: ( ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ) implies x in F4(F2()) \/ F4(F3()) )
proof
assume x in F4(F2()) \/ F4(F3()) ; :: thesis: ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } )
per cases then ( x in F4(F2()) or x in F4(F3()) ) by XBOOLE_0:def 3;
suppose A1: x in F4(F2()) ; :: thesis: ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } )
take F4(F2()) ; :: thesis: ( x in F4(F2()) & F4(F2()) in { F4(j) where j is Element of F1() : j in {F2(),F3()} } )
thus x in F4(F2()) by A1; :: thesis: F4(F2()) in { F4(j) where j is Element of F1() : j in {F2(),F3()} }
F2() in {F2(),F3()} by TARSKI:def 2;
hence F4(F2()) in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ; :: thesis: verum
end;
suppose A2: x in F4(F3()) ; :: thesis: ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } )
take F4(F3()) ; :: thesis: ( x in F4(F3()) & F4(F3()) in { F4(j) where j is Element of F1() : j in {F2(),F3()} } )
thus x in F4(F3()) by A2; :: thesis: F4(F3()) in { F4(j) where j is Element of F1() : j in {F2(),F3()} }
F3() in {F2(),F3()} by TARSKI:def 2;
hence F4(F3()) in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ; :: thesis: verum
end;
end;
end;
given Y being set such that A3: x in Y and
A4: Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ; :: thesis: x in F4(F2()) \/ F4(F3())
consider j being Element of F1() such that
A5: Y = F4(j) and
A6: j in {F2(),F3()} by A4;
now :: thesis: ( ( j = F2() & x in F4(F2()) ) or ( j = F3() & x in F4(F3()) ) )
per cases ( j = F2() or j = F3() ) by A6, TARSKI:def 2;
case j = F2() ; :: thesis: x in F4(F2())
hence x in F4(F2()) by A3, A5; :: thesis: verum
end;
case j = F3() ; :: thesis: x in F4(F3())
hence x in F4(F3()) by A3, A5; :: thesis: verum
end;
end;
end;
hence x in F4(F2()) \/ F4(F3()) by XBOOLE_0:def 3; :: thesis: verum
end;
hence union { F4(j) where j is Element of F1() : j in {F2(),F3()} } = F4(F2()) \/ F4(F3()) by TARSKI:def 4; :: thesis: verum