set Q = F1();
set X = F3();
set Y = F4();
set Z = { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } ;
set W = { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } ;
set S = { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ;
A1:
{ ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } = { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() }
proof
thus
{ ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } c= { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() }
XBOOLE_0:def 10 { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } c= { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } proof
let x be
object ;
TARSKI:def 3 ( not x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } or x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } )
assume
x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } }
;
x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() }
then consider V being
Subset of
F1()
such that A2:
x = "\/" V
and A3:
V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
;
ex
a being
Element of
F1() st
(
V = { F2(a,b) where b is Element of F1() : b in F4() } &
a in F3() )
by A3;
hence
x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() }
by A2;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } or x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } } )
assume
x in { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() }
;
x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } }
then consider a being
Element of
F1()
such that A4:
x = "\/" (
{ F2(a,b) where b is Element of F1() : b in F4() } ,
F1())
and A5:
a in F3()
;
A6:
{ F2(a,b) where b is Element of F1() : b in F4() } c= H1(
F1())
{ F2(a,c) where c is Element of F1() : c in F4() } in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
by A5;
hence
x in { ("\/" V) where V is Subset of F1() : V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } }
by A4, A6;
verum
end;
A7:
{ F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } = union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
proof
thus
{ F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } c= union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
XBOOLE_0:def 10 union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } c= { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } proof
let x be
object ;
TARSKI:def 3 ( not x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } or x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } )
assume
x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) }
;
x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
then consider a,
b being
Element of
F1()
such that A8:
(
x = F2(
a,
b) &
a in F3() &
b in F4() )
;
(
x in { F2(a,c) where c is Element of F1() : c in F4() } &
{ F2(a,d) where d is Element of F1() : d in F4() } in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } )
by A8;
hence
x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
by TARSKI:def 4;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } or x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } )
assume
x in union { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
;
x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) }
then consider V being
set such that A9:
x in V
and A10:
V in { { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() }
by TARSKI:def 4;
consider a being
Element of
F1()
such that A11:
V = { F2(a,b) where b is Element of F1() : b in F4() }
and A12:
a in F3()
by A10;
ex
b being
Element of
F1() st
(
x = F2(
a,
b) &
b in F4() )
by A9, A11;
hence
x in { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) }
by A12;
verum
end;
{ { F2(a,b) where b is Element of F1() : b in F4() } where a is Element of F1() : a in F3() } c= bool H1(F1())
hence
"\/" ( { ("\/" ( { F2(a,b) where b is Element of F1() : b in F4() } ,F1())) where a is Element of F1() : a in F3() } ,F1()) = "\/" ( { F2(a,b) where a, b is Element of F1() : ( a in F3() & b in F4() ) } ,F1())
by A1, A7, LATTICE3:48; verum