Step |
Hyp |
Ref |
Expression |
1 |
|
isldsys.l |
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) } |
2 |
|
ldsysgenld.1 |
|- ( ph -> O e. V ) |
3 |
|
ldsysgenld.2 |
|- ( ph -> A C_ ~P O ) |
4 |
|
pwsiga |
|- ( O e. V -> ~P O e. ( sigAlgebra ` O ) ) |
5 |
2 4
|
syl |
|- ( ph -> ~P O e. ( sigAlgebra ` O ) ) |
6 |
1
|
sigaldsys |
|- ( sigAlgebra ` O ) C_ L |
7 |
6 5
|
sseldi |
|- ( ph -> ~P O e. L ) |
8 |
|
sseq2 |
|- ( t = ~P O -> ( A C_ t <-> A C_ ~P O ) ) |
9 |
8
|
elrab |
|- ( ~P O e. { t e. L | A C_ t } <-> ( ~P O e. L /\ A C_ ~P O ) ) |
10 |
7 3 9
|
sylanbrc |
|- ( ph -> ~P O e. { t e. L | A C_ t } ) |
11 |
|
intss1 |
|- ( ~P O e. { t e. L | A C_ t } -> |^| { t e. L | A C_ t } C_ ~P O ) |
12 |
10 11
|
syl |
|- ( ph -> |^| { t e. L | A C_ t } C_ ~P O ) |
13 |
5 12
|
sselpwd |
|- ( ph -> |^| { t e. L | A C_ t } e. ~P ~P O ) |
14 |
1
|
isldsys |
|- ( t e. L <-> ( t e. ~P ~P O /\ ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) ) ) |
15 |
14
|
simprbi |
|- ( t e. L -> ( (/) e. t /\ A. x e. t ( O \ x ) e. t /\ A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) ) |
16 |
15
|
simp1d |
|- ( t e. L -> (/) e. t ) |
17 |
16
|
adantl |
|- ( ( ph /\ t e. L ) -> (/) e. t ) |
18 |
17
|
a1d |
|- ( ( ph /\ t e. L ) -> ( A C_ t -> (/) e. t ) ) |
19 |
18
|
ralrimiva |
|- ( ph -> A. t e. L ( A C_ t -> (/) e. t ) ) |
20 |
|
0ex |
|- (/) e. _V |
21 |
20
|
elintrab |
|- ( (/) e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> (/) e. t ) ) |
22 |
19 21
|
sylibr |
|- ( ph -> (/) e. |^| { t e. L | A C_ t } ) |
23 |
|
nfv |
|- F/ t ph |
24 |
|
nfcv |
|- F/_ t x |
25 |
|
nfrab1 |
|- F/_ t { t e. L | A C_ t } |
26 |
25
|
nfint |
|- F/_ t |^| { t e. L | A C_ t } |
27 |
24 26
|
nfel |
|- F/ t x e. |^| { t e. L | A C_ t } |
28 |
23 27
|
nfan |
|- F/ t ( ph /\ x e. |^| { t e. L | A C_ t } ) |
29 |
|
simplr |
|- ( ( ( ( ph /\ x e. |^| { t e. L | A C_ t } ) /\ t e. L ) /\ A C_ t ) -> t e. L ) |
30 |
|
vex |
|- x e. _V |
31 |
30
|
elintrab |
|- ( x e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> x e. t ) ) |
32 |
31
|
biimpi |
|- ( x e. |^| { t e. L | A C_ t } -> A. t e. L ( A C_ t -> x e. t ) ) |
33 |
32
|
adantl |
|- ( ( ph /\ x e. |^| { t e. L | A C_ t } ) -> A. t e. L ( A C_ t -> x e. t ) ) |
34 |
33
|
r19.21bi |
|- ( ( ( ph /\ x e. |^| { t e. L | A C_ t } ) /\ t e. L ) -> ( A C_ t -> x e. t ) ) |
35 |
34
|
imp |
|- ( ( ( ( ph /\ x e. |^| { t e. L | A C_ t } ) /\ t e. L ) /\ A C_ t ) -> x e. t ) |
36 |
15
|
simp2d |
|- ( t e. L -> A. x e. t ( O \ x ) e. t ) |
37 |
36
|
r19.21bi |
|- ( ( t e. L /\ x e. t ) -> ( O \ x ) e. t ) |
38 |
29 35 37
|
syl2anc |
|- ( ( ( ( ph /\ x e. |^| { t e. L | A C_ t } ) /\ t e. L ) /\ A C_ t ) -> ( O \ x ) e. t ) |
39 |
38
|
ex |
|- ( ( ( ph /\ x e. |^| { t e. L | A C_ t } ) /\ t e. L ) -> ( A C_ t -> ( O \ x ) e. t ) ) |
40 |
39
|
ex |
|- ( ( ph /\ x e. |^| { t e. L | A C_ t } ) -> ( t e. L -> ( A C_ t -> ( O \ x ) e. t ) ) ) |
41 |
28 40
|
ralrimi |
|- ( ( ph /\ x e. |^| { t e. L | A C_ t } ) -> A. t e. L ( A C_ t -> ( O \ x ) e. t ) ) |
42 |
|
difexg |
|- ( O e. V -> ( O \ x ) e. _V ) |
43 |
|
elintrabg |
|- ( ( O \ x ) e. _V -> ( ( O \ x ) e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> ( O \ x ) e. t ) ) ) |
44 |
2 42 43
|
3syl |
|- ( ph -> ( ( O \ x ) e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> ( O \ x ) e. t ) ) ) |
45 |
44
|
adantr |
|- ( ( ph /\ x e. |^| { t e. L | A C_ t } ) -> ( ( O \ x ) e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> ( O \ x ) e. t ) ) ) |
46 |
41 45
|
mpbird |
|- ( ( ph /\ x e. |^| { t e. L | A C_ t } ) -> ( O \ x ) e. |^| { t e. L | A C_ t } ) |
47 |
46
|
ralrimiva |
|- ( ph -> A. x e. |^| { t e. L | A C_ t } ( O \ x ) e. |^| { t e. L | A C_ t } ) |
48 |
26
|
nfpw |
|- F/_ t ~P |^| { t e. L | A C_ t } |
49 |
24 48
|
nfel |
|- F/ t x e. ~P |^| { t e. L | A C_ t } |
50 |
23 49
|
nfan |
|- F/ t ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) |
51 |
|
nfv |
|- F/ t ( x ~<_ _om /\ Disj_ y e. x y ) |
52 |
50 51
|
nfan |
|- F/ t ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) |
53 |
|
simplr |
|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> t e. L ) |
54 |
|
simpr |
|- ( ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) /\ u e. |^| { t e. L | A C_ t } ) -> u e. |^| { t e. L | A C_ t } ) |
55 |
|
simpllr |
|- ( ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) /\ u e. |^| { t e. L | A C_ t } ) -> t e. L ) |
56 |
|
simplr |
|- ( ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) /\ u e. |^| { t e. L | A C_ t } ) -> A C_ t ) |
57 |
|
vex |
|- u e. _V |
58 |
57
|
elintrab |
|- ( u e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> u e. t ) ) |
59 |
58
|
biimpi |
|- ( u e. |^| { t e. L | A C_ t } -> A. t e. L ( A C_ t -> u e. t ) ) |
60 |
59
|
r19.21bi |
|- ( ( u e. |^| { t e. L | A C_ t } /\ t e. L ) -> ( A C_ t -> u e. t ) ) |
61 |
60
|
imp |
|- ( ( ( u e. |^| { t e. L | A C_ t } /\ t e. L ) /\ A C_ t ) -> u e. t ) |
62 |
54 55 56 61
|
syl21anc |
|- ( ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) /\ u e. |^| { t e. L | A C_ t } ) -> u e. t ) |
63 |
62
|
ex |
|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> ( u e. |^| { t e. L | A C_ t } -> u e. t ) ) |
64 |
63
|
ssrdv |
|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> |^| { t e. L | A C_ t } C_ t ) |
65 |
64
|
sspwd |
|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> ~P |^| { t e. L | A C_ t } C_ ~P t ) |
66 |
|
simp-4r |
|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> x e. ~P |^| { t e. L | A C_ t } ) |
67 |
65 66
|
sseldd |
|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> x e. ~P t ) |
68 |
|
simpllr |
|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> ( x ~<_ _om /\ Disj_ y e. x y ) ) |
69 |
15
|
simp3d |
|- ( t e. L -> A. x e. ~P t ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) |
70 |
69
|
r19.21bi |
|- ( ( t e. L /\ x e. ~P t ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. t ) ) |
71 |
70
|
imp |
|- ( ( ( t e. L /\ x e. ~P t ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> U. x e. t ) |
72 |
53 67 68 71
|
syl21anc |
|- ( ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) /\ A C_ t ) -> U. x e. t ) |
73 |
72
|
ex |
|- ( ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) /\ t e. L ) -> ( A C_ t -> U. x e. t ) ) |
74 |
73
|
ex |
|- ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( t e. L -> ( A C_ t -> U. x e. t ) ) ) |
75 |
52 74
|
ralrimi |
|- ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> A. t e. L ( A C_ t -> U. x e. t ) ) |
76 |
|
vuniex |
|- U. x e. _V |
77 |
76
|
elintrab |
|- ( U. x e. |^| { t e. L | A C_ t } <-> A. t e. L ( A C_ t -> U. x e. t ) ) |
78 |
75 77
|
sylibr |
|- ( ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> U. x e. |^| { t e. L | A C_ t } ) |
79 |
78
|
ex |
|- ( ( ph /\ x e. ~P |^| { t e. L | A C_ t } ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. |^| { t e. L | A C_ t } ) ) |
80 |
79
|
ralrimiva |
|- ( ph -> A. x e. ~P |^| { t e. L | A C_ t } ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. |^| { t e. L | A C_ t } ) ) |
81 |
22 47 80
|
3jca |
|- ( ph -> ( (/) e. |^| { t e. L | A C_ t } /\ A. x e. |^| { t e. L | A C_ t } ( O \ x ) e. |^| { t e. L | A C_ t } /\ A. x e. ~P |^| { t e. L | A C_ t } ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. |^| { t e. L | A C_ t } ) ) ) |
82 |
13 81
|
jca |
|- ( ph -> ( |^| { t e. L | A C_ t } e. ~P ~P O /\ ( (/) e. |^| { t e. L | A C_ t } /\ A. x e. |^| { t e. L | A C_ t } ( O \ x ) e. |^| { t e. L | A C_ t } /\ A. x e. ~P |^| { t e. L | A C_ t } ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. |^| { t e. L | A C_ t } ) ) ) ) |
83 |
1
|
isldsys |
|- ( |^| { t e. L | A C_ t } e. L <-> ( |^| { t e. L | A C_ t } e. ~P ~P O /\ ( (/) e. |^| { t e. L | A C_ t } /\ A. x e. |^| { t e. L | A C_ t } ( O \ x ) e. |^| { t e. L | A C_ t } /\ A. x e. ~P |^| { t e. L | A C_ t } ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. |^| { t e. L | A C_ t } ) ) ) ) |
84 |
82 83
|
sylibr |
|- ( ph -> |^| { t e. L | A C_ t } e. L ) |