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