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;
then A8:
{ (x \/ y) where x, y is Element of V : ( x in D2 & y in F2 ) } in X
by A4, A6;
now for p being object st 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 ) } holds
p in Diagram ((H '&' H9),E)let p be
object ;
( 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),E)then
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, Def4;
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, Def4;
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:13, XBOOLE_1:79;
rng gg = (rng ((f * decode) | (code (Free H)))) \/ (rng e)
by RELAT_1:12;
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, XTUPLE_0:23;
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:2;
now ( code (Free H9) = dom ((ff * decode) | (code (Free H9))) & dom ((g * decode) | (code (Free H9))) = code (Free H9) & ( for q being object st q in code (Free H9) holds
((ff * decode) | (code (Free H9))) . q = ((g * decode) | (code (Free H9))) . q ) )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 object st q in code (Free H9) holds
((ff * decode) | (code (Free H9))) . q = ((g * decode) | (code (Free H9))) . qlet q be
object ;
( 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:78;
hence ((ff * decode) | (code (Free H9))) . q =
((ff * decode) | ((code (Free H)) \/ (code (Free H9)))) . q
by A29, A30, GRFUNC_1:15
.=
((g * decode) | (code (Free H9))) . q
by A10, A13, A15, A21, A16, A18, A25, A29, A30, GRFUNC_1:15
;
verum end; then
ff in St (
H9,
E)
by A17, Lm10, FUNCT_1:2;
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:120
.=
(ff * decode) | (code (Free (H '&' H9)))
by ZF_LANG1:61
;
hence
p in Diagram (
(H '&' H9),
E)
by A31, Def4;
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)
;
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
object ;
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 Def4;
f in St (
H9,
E)
by A34, ZF_MODEL:5;
then A35:
(f * decode) | (code (Free H9)) in D2
by Def4;
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:32;
then A36:
(f * decode) | ((code (Free H)) \ (code (Free H9))) in F2
by FUNCT_2:8;
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:61;
then p =
(f * decode) | ((code (Free H9)) \/ (code (Free H)))
by A33, RELAT_1:120
.=
(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:78
;
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 Def4;
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:32;
then A40:
(f * decode) | ((code (Free H9)) \ (code (Free H))) in F1
by FUNCT_2:8;
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:120
.=
(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:78
;
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;
{ (x \/ y) where x, y is Element of V : ( x in D1 & y in F1 ) } in X
by A3, A5, A7;
hence
Diagram ((H '&' H9),E) in X
by A1, A8, A41, Th5; verum