let V be Universe; for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 & E in X holds
for H, H9 being ZF-formula st Diagram H,E in X & Diagram H9,E in X holds
Diagram (H '&' H9),E in X
let X be Subclass of V; for E being non empty set st X is closed_wrt_A1-A7 & E in X holds
for H, H9 being ZF-formula st Diagram H,E in X & Diagram H9,E in X holds
Diagram (H '&' H9),E in X
let E be non empty set ; ( X is closed_wrt_A1-A7 & E in X implies for H, H9 being ZF-formula st Diagram H,E in X & Diagram H9,E in X holds
Diagram (H '&' H9),E in X )
assume that
A1:
X is closed_wrt_A1-A7
and
A2:
E in X
; for H, H9 being ZF-formula st Diagram H,E in X & Diagram H9,E in X holds
Diagram (H '&' H9),E in X
reconsider E9 = E as Element of V by A2;
let H, H9 be ZF-formula; ( Diagram H,E in X & Diagram H9,E in X implies Diagram (H '&' H9),E in X )
assume that
A3:
Diagram H,E in X
and
A4:
Diagram H9,E in X
; Diagram (H '&' H9),E in X
set fs = code (Free H);
set fs9 = code (Free H9);
reconsider D1 = Diagram H,E, D2 = Diagram H9,E as Element of V by A3, A4;
A5:
Funcs ((code (Free H9)) \ (code (Free H))),E9 in X
by A1, A2, Th9;
then reconsider F1 = Funcs ((code (Free H9)) \ (code (Free H))),E9 as Element of V ;
A6:
Funcs ((code (Free H)) \ (code (Free H9))),E9 in X
by A1, A2, Th9;
then reconsider F2 = Funcs ((code (Free H)) \ (code (Free H9))),E9 as Element of V ;
set A = { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } ;
set B = { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } ;
A7:
X is closed_wrt_A5
by A1, Def13;
then A8:
{ (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } in X
by A4, A6, Def10;
now consider h being
Function;
let p be
set ;
( p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } implies p in Diagram (H '&' H9),E )assume A9:
p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) }
;
p in Diagram (H '&' H9),Ethen
p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) }
by XBOOLE_0:def 4;
then consider x,
y being
Element of
V such that A10:
p = x \/ y
and A11:
x in D1
and A12:
y in F1
;
p in { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) }
by A9, XBOOLE_0:def 4;
then consider x9,
y9 being
Element of
V such that A13:
p = x9 \/ y9
and A14:
x9 in D2
and A15:
y9 in F2
;
consider g being
Function of
VAR ,
E such that A16:
x9 = (g * decode ) | (code (Free H9))
and A17:
g in St H9,
E
by A14, Def5;
consider e being
Function such that A18:
y = e
and A19:
dom e = (code (Free H9)) \ (code (Free H))
and A20:
rng e c= E
by A12, FUNCT_2:def 2;
consider f being
Function of
VAR ,
E such that A21:
x = (f * decode ) | (code (Free H))
and A22:
f in St H,
E
by A11, Def5;
A23:
dom ((f * decode ) | (code (Free H))) = code (Free H)
by Lm3;
then reconsider gg =
((f * decode ) | (code (Free H))) \/ e as
Function by A19, GRFUNC_1:31, XBOOLE_1:79;
rng gg = (rng ((f * decode ) | (code (Free H)))) \/ (rng e)
by RELAT_1:26;
then A24:
rng gg c= E
by A20, XBOOLE_1:8;
dom gg = (code (Free H)) \/ ((code (Free H9)) \ (code (Free H)))
by A19, A23, RELAT_1:13;
then
dom gg = (code (Free H)) \/ (code (Free H9))
by XBOOLE_1:39;
then
gg in Funcs ((code (Free H)) \/ (code (Free H9))),
E
by A24, FUNCT_2:def 2;
then consider ff being
Function of
VAR ,
E such that A25:
gg = (ff * decode ) | ((code (Free H)) \/ (code (Free H9)))
by Lm11;
then A28:
ff in St H,
E
by A22, Lm10, FUNCT_1:9;
now thus A29:
(
code (Free H9) = dom ((ff * decode ) | (code (Free H9))) &
dom ((g * decode ) | (code (Free H9))) = code (Free H9) )
by Lm3;
for q being set st q in code (Free H9) holds
((ff * decode ) | (code (Free H9))) . q = ((g * decode ) | (code (Free H9))) . qlet q be
set ;
( q in code (Free H9) implies ((ff * decode ) | (code (Free H9))) . q = ((g * decode ) | (code (Free H9))) . q )assume A30:
q in code (Free H9)
;
((ff * decode ) | (code (Free H9))) . q = ((g * decode ) | (code (Free H9))) . q
(ff * decode ) | ((code (Free H)) \/ (code (Free H9))) = ((ff * decode ) | (code (Free H))) \/ ((ff * decode ) | (code (Free H9)))
by RELAT_1:107;
hence ((ff * decode ) | (code (Free H9))) . q =
((ff * decode ) | ((code (Free H)) \/ (code (Free H9)))) . q
by A29, A30, GRFUNC_1:35
.=
((g * decode ) | (code (Free H9))) . q
by A10, A13, A15, A21, A16, A18, A25, A29, A30, GRFUNC_1:35
;
verum end; then
ff in St H9,
E
by A17, Lm10, FUNCT_1:9;
then A31:
ff in St (H '&' H9),
E
by A28, ZF_MODEL:5;
p =
(ff * decode ) | (code ((Free H) \/ (Free H9)))
by A10, A21, A18, A25, RELAT_1:153
.=
(ff * decode ) | (code (Free (H '&' H9)))
by ZF_LANG1:66
;
hence
p in Diagram (H '&' H9),
E
by A31, Def5;
verum end;
then A32:
{ (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } c= Diagram (H '&' H9),E
by TARSKI:def 3;
Diagram (H '&' H9),E c= { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) }
proof
let p be
set ;
TARSKI:def 3 ( not p in Diagram (H '&' H9),E or p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } )
assume
p in Diagram (H '&' H9),
E
;
p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) }
then consider f being
Function of
VAR ,
E such that A33:
p = (f * decode ) | (code (Free (H '&' H9)))
and A34:
f in St (H '&' H9),
E
by Def5;
f in St H9,
E
by A34, ZF_MODEL:5;
then A35:
(f * decode ) | (code (Free H9)) in D2
by Def5;
then reconsider z =
(f * decode ) | (code (Free H9)) as
Element of
V by A4, Th1;
(f * decode ) | ((code (Free H)) \ (code (Free H9))) is
Function of
((code (Free H)) \ (code (Free H9))),
E
by FUNCT_2:38;
then A36:
(f * decode ) | ((code (Free H)) \ (code (Free H9))) in F2
by FUNCT_2:11;
then reconsider t =
(f * decode ) | ((code (Free H)) \ (code (Free H9))) as
Element of
V by A6, Th1;
A37:
Free (H '&' H9) = (Free H) \/ (Free H9)
by ZF_LANG1:66;
then p =
(f * decode ) | ((code (Free H9)) \/ (code (Free H)))
by A33, RELAT_1:153
.=
(f * decode ) | ((code (Free H9)) \/ ((code (Free H)) \ (code (Free H9))))
by XBOOLE_1:39
.=
((f * decode ) | (code (Free H9))) \/ ((f * decode ) | ((code (Free H)) \ (code (Free H9))))
by RELAT_1:107
;
then
p = z \/ t
;
then A38:
p in { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) }
by A35, A36;
f in St H,
E
by A34, ZF_MODEL:5;
then A39:
(f * decode ) | (code (Free H)) in D1
by Def5;
then reconsider x =
(f * decode ) | (code (Free H)) as
Element of
V by A3, Th1;
(f * decode ) | ((code (Free H9)) \ (code (Free H))) is
Function of
((code (Free H9)) \ (code (Free H))),
E
by FUNCT_2:38;
then A40:
(f * decode ) | ((code (Free H9)) \ (code (Free H))) in F1
by FUNCT_2:11;
then reconsider y =
(f * decode ) | ((code (Free H9)) \ (code (Free H))) as
Element of
V by A5, Th1;
p =
(f * decode ) | ((code (Free H)) \/ (code (Free H9)))
by A33, A37, RELAT_1:153
.=
(f * decode ) | ((code (Free H)) \/ ((code (Free H9)) \ (code (Free H))))
by XBOOLE_1:39
.=
((f * decode ) | (code (Free H))) \/ ((f * decode ) | ((code (Free H9)) \ (code (Free H))))
by RELAT_1:107
;
then
p = x \/ y
;
then
p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) }
by A39, A40;
hence
p in { (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) }
by A38, XBOOLE_0:def 4;
verum
end;
then A41:
{ (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } /\ { (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } = Diagram (H '&' H9),E
by A32, XBOOLE_0:def 10;
{ (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } in X
by A3, A5, A7, Def10;
hence
Diagram (H '&' H9),E in X
by A1, A8, A41, Th5; verum