Step |
Hyp |
Ref |
Expression |
1 |
|
alexsubALT.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
ssel |
⊢ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) ) |
3 |
|
elun |
⊢ ( 𝑤 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ↔ ( 𝑤 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∨ 𝑤 ∈ { ∅ } ) ) |
4 |
|
sseq2 |
⊢ ( 𝑧 = 𝑤 → ( 𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑤 ) ) |
5 |
|
pweq |
⊢ ( 𝑧 = 𝑤 → 𝒫 𝑧 = 𝒫 𝑤 ) |
6 |
5
|
ineq1d |
⊢ ( 𝑧 = 𝑤 → ( 𝒫 𝑧 ∩ Fin ) = ( 𝒫 𝑤 ∩ Fin ) ) |
7 |
6
|
raleqdv |
⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) |
8 |
4 7
|
anbi12d |
⊢ ( 𝑧 = 𝑤 → ( ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ↔ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
9 |
8
|
elrab |
⊢ ( 𝑤 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ↔ ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
10 |
|
velsn |
⊢ ( 𝑤 ∈ { ∅ } ↔ 𝑤 = ∅ ) |
11 |
9 10
|
orbi12i |
⊢ ( ( 𝑤 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∨ 𝑤 ∈ { ∅ } ) ↔ ( ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ∨ 𝑤 = ∅ ) ) |
12 |
3 11
|
bitri |
⊢ ( 𝑤 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ↔ ( ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ∨ 𝑤 = ∅ ) ) |
13 |
|
elpwi |
⊢ ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) → 𝑤 ⊆ ( fi ‘ 𝑥 ) ) |
14 |
13
|
adantr |
⊢ ( ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → 𝑤 ⊆ ( fi ‘ 𝑥 ) ) |
15 |
|
0ss |
⊢ ∅ ⊆ ( fi ‘ 𝑥 ) |
16 |
|
sseq1 |
⊢ ( 𝑤 = ∅ → ( 𝑤 ⊆ ( fi ‘ 𝑥 ) ↔ ∅ ⊆ ( fi ‘ 𝑥 ) ) ) |
17 |
15 16
|
mpbiri |
⊢ ( 𝑤 = ∅ → 𝑤 ⊆ ( fi ‘ 𝑥 ) ) |
18 |
14 17
|
jaoi |
⊢ ( ( ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ∨ 𝑤 = ∅ ) → 𝑤 ⊆ ( fi ‘ 𝑥 ) ) |
19 |
12 18
|
sylbi |
⊢ ( 𝑤 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → 𝑤 ⊆ ( fi ‘ 𝑥 ) ) |
20 |
2 19
|
syl6 |
⊢ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ( 𝑤 ∈ 𝑦 → 𝑤 ⊆ ( fi ‘ 𝑥 ) ) ) |
21 |
20
|
ralrimiv |
⊢ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ∀ 𝑤 ∈ 𝑦 𝑤 ⊆ ( fi ‘ 𝑥 ) ) |
22 |
|
unissb |
⊢ ( ∪ 𝑦 ⊆ ( fi ‘ 𝑥 ) ↔ ∀ 𝑤 ∈ 𝑦 𝑤 ⊆ ( fi ‘ 𝑥 ) ) |
23 |
21 22
|
sylibr |
⊢ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ∪ 𝑦 ⊆ ( fi ‘ 𝑥 ) ) |
24 |
23
|
adantr |
⊢ ( ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ⊆ ( fi ‘ 𝑥 ) ) |
25 |
24
|
ad2antlr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ¬ ∪ 𝑦 = ∅ ) → ∪ 𝑦 ⊆ ( fi ‘ 𝑥 ) ) |
26 |
|
vuniex |
⊢ ∪ 𝑦 ∈ V |
27 |
26
|
elpw |
⊢ ( ∪ 𝑦 ∈ 𝒫 ( fi ‘ 𝑥 ) ↔ ∪ 𝑦 ⊆ ( fi ‘ 𝑥 ) ) |
28 |
25 27
|
sylibr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ¬ ∪ 𝑦 = ∅ ) → ∪ 𝑦 ∈ 𝒫 ( fi ‘ 𝑥 ) ) |
29 |
|
uni0b |
⊢ ( ∪ 𝑦 = ∅ ↔ 𝑦 ⊆ { ∅ } ) |
30 |
29
|
notbii |
⊢ ( ¬ ∪ 𝑦 = ∅ ↔ ¬ 𝑦 ⊆ { ∅ } ) |
31 |
|
disjssun |
⊢ ( ( 𝑦 ∩ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) = ∅ → ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ↔ 𝑦 ⊆ { ∅ } ) ) |
32 |
31
|
biimpcd |
⊢ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ( ( 𝑦 ∩ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) = ∅ → 𝑦 ⊆ { ∅ } ) ) |
33 |
32
|
necon3bd |
⊢ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ( ¬ 𝑦 ⊆ { ∅ } → ( 𝑦 ∩ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ≠ ∅ ) ) |
34 |
|
n0 |
⊢ ( ( 𝑦 ∩ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝑦 ∩ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ) |
35 |
|
elin |
⊢ ( 𝑤 ∈ ( 𝑦 ∩ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ↔ ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ) |
36 |
9
|
anbi2i |
⊢ ( ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ↔ ( 𝑤 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ) |
37 |
35 36
|
bitri |
⊢ ( 𝑤 ∈ ( 𝑦 ∩ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ↔ ( 𝑤 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ) |
38 |
|
simprrl |
⊢ ( ( 𝑤 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → 𝑎 ⊆ 𝑤 ) |
39 |
|
simpl |
⊢ ( ( 𝑤 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → 𝑤 ∈ 𝑦 ) |
40 |
|
ssuni |
⊢ ( ( 𝑎 ⊆ 𝑤 ∧ 𝑤 ∈ 𝑦 ) → 𝑎 ⊆ ∪ 𝑦 ) |
41 |
38 39 40
|
syl2anc |
⊢ ( ( 𝑤 ∈ 𝑦 ∧ ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) → 𝑎 ⊆ ∪ 𝑦 ) |
42 |
37 41
|
sylbi |
⊢ ( 𝑤 ∈ ( 𝑦 ∩ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) → 𝑎 ⊆ ∪ 𝑦 ) |
43 |
42
|
exlimiv |
⊢ ( ∃ 𝑤 𝑤 ∈ ( 𝑦 ∩ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) → 𝑎 ⊆ ∪ 𝑦 ) |
44 |
34 43
|
sylbi |
⊢ ( ( 𝑦 ∩ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ≠ ∅ → 𝑎 ⊆ ∪ 𝑦 ) |
45 |
33 44
|
syl6 |
⊢ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ( ¬ 𝑦 ⊆ { ∅ } → 𝑎 ⊆ ∪ 𝑦 ) ) |
46 |
45
|
ad2antrl |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) → ( ¬ 𝑦 ⊆ { ∅ } → 𝑎 ⊆ ∪ 𝑦 ) ) |
47 |
30 46
|
syl5bi |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) → ( ¬ ∪ 𝑦 = ∅ → 𝑎 ⊆ ∪ 𝑦 ) ) |
48 |
47
|
imp |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ¬ ∪ 𝑦 = ∅ ) → 𝑎 ⊆ ∪ 𝑦 ) |
49 |
|
elfpw |
⊢ ( 𝑛 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ↔ ( 𝑛 ⊆ ∪ 𝑦 ∧ 𝑛 ∈ Fin ) ) |
50 |
|
unieq |
⊢ ( 𝑦 = ∅ → ∪ 𝑦 = ∪ ∅ ) |
51 |
|
uni0 |
⊢ ∪ ∅ = ∅ |
52 |
50 51
|
eqtrdi |
⊢ ( 𝑦 = ∅ → ∪ 𝑦 = ∅ ) |
53 |
52
|
necon3bi |
⊢ ( ¬ ∪ 𝑦 = ∅ → 𝑦 ≠ ∅ ) |
54 |
53
|
adantr |
⊢ ( ( ¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin ) → 𝑦 ≠ ∅ ) |
55 |
54
|
ad2antrl |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ( ( ¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin ) ∧ 𝑛 ⊆ ∪ 𝑦 ) ) → 𝑦 ≠ ∅ ) |
56 |
|
simplrr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ( ( ¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin ) ∧ 𝑛 ⊆ ∪ 𝑦 ) ) → [⊊] Or 𝑦 ) |
57 |
|
simprlr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ( ( ¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin ) ∧ 𝑛 ⊆ ∪ 𝑦 ) ) → 𝑛 ∈ Fin ) |
58 |
|
simprr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ( ( ¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin ) ∧ 𝑛 ⊆ ∪ 𝑦 ) ) → 𝑛 ⊆ ∪ 𝑦 ) |
59 |
|
finsschain |
⊢ ( ( ( 𝑦 ≠ ∅ ∧ [⊊] Or 𝑦 ) ∧ ( 𝑛 ∈ Fin ∧ 𝑛 ⊆ ∪ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤 ) |
60 |
55 56 57 58 59
|
syl22anc |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ( ( ¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin ) ∧ 𝑛 ⊆ ∪ 𝑦 ) ) → ∃ 𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤 ) |
61 |
60
|
expr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ( ¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin ) ) → ( 𝑛 ⊆ ∪ 𝑦 → ∃ 𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤 ) ) |
62 |
|
0elpw |
⊢ ∅ ∈ 𝒫 𝑎 |
63 |
|
0fin |
⊢ ∅ ∈ Fin |
64 |
62 63
|
elini |
⊢ ∅ ∈ ( 𝒫 𝑎 ∩ Fin ) |
65 |
|
unieq |
⊢ ( 𝑏 = ∅ → ∪ 𝑏 = ∪ ∅ ) |
66 |
65
|
eqeq2d |
⊢ ( 𝑏 = ∅ → ( 𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ ∅ ) ) |
67 |
66
|
notbid |
⊢ ( 𝑏 = ∅ → ( ¬ 𝑋 = ∪ 𝑏 ↔ ¬ 𝑋 = ∪ ∅ ) ) |
68 |
67
|
rspccv |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( ∅ ∈ ( 𝒫 𝑎 ∩ Fin ) → ¬ 𝑋 = ∪ ∅ ) ) |
69 |
64 68
|
mpi |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ¬ 𝑋 = ∪ ∅ ) |
70 |
|
velpw |
⊢ ( 𝑛 ∈ 𝒫 𝑤 ↔ 𝑛 ⊆ 𝑤 ) |
71 |
|
elin |
⊢ ( 𝑛 ∈ ( 𝒫 𝑤 ∩ Fin ) ↔ ( 𝑛 ∈ 𝒫 𝑤 ∧ 𝑛 ∈ Fin ) ) |
72 |
|
unieq |
⊢ ( 𝑏 = 𝑛 → ∪ 𝑏 = ∪ 𝑛 ) |
73 |
72
|
eqeq2d |
⊢ ( 𝑏 = 𝑛 → ( 𝑋 = ∪ 𝑏 ↔ 𝑋 = ∪ 𝑛 ) ) |
74 |
73
|
notbid |
⊢ ( 𝑏 = 𝑛 → ( ¬ 𝑋 = ∪ 𝑏 ↔ ¬ 𝑋 = ∪ 𝑛 ) ) |
75 |
74
|
rspccv |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑛 ∈ ( 𝒫 𝑤 ∩ Fin ) → ¬ 𝑋 = ∪ 𝑛 ) ) |
76 |
71 75
|
syl5bir |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( ( 𝑛 ∈ 𝒫 𝑤 ∧ 𝑛 ∈ Fin ) → ¬ 𝑋 = ∪ 𝑛 ) ) |
77 |
76
|
expd |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑛 ∈ 𝒫 𝑤 → ( 𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛 ) ) ) |
78 |
70 77
|
syl5bir |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑛 ⊆ 𝑤 → ( 𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛 ) ) ) |
79 |
78
|
com23 |
⊢ ( ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 → ( 𝑛 ∈ Fin → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) |
80 |
79
|
ad2antll |
⊢ ( ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → ( 𝑛 ∈ Fin → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) |
81 |
80
|
a1i |
⊢ ( ¬ 𝑋 = ∪ ∅ → ( ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) → ( 𝑛 ∈ Fin → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
82 |
|
sseq2 |
⊢ ( 𝑤 = ∅ → ( 𝑛 ⊆ 𝑤 ↔ 𝑛 ⊆ ∅ ) ) |
83 |
|
ss0 |
⊢ ( 𝑛 ⊆ ∅ → 𝑛 = ∅ ) |
84 |
82 83
|
syl6bi |
⊢ ( 𝑤 = ∅ → ( 𝑛 ⊆ 𝑤 → 𝑛 = ∅ ) ) |
85 |
|
unieq |
⊢ ( 𝑛 = ∅ → ∪ 𝑛 = ∪ ∅ ) |
86 |
85
|
eqeq2d |
⊢ ( 𝑛 = ∅ → ( 𝑋 = ∪ 𝑛 ↔ 𝑋 = ∪ ∅ ) ) |
87 |
86
|
notbid |
⊢ ( 𝑛 = ∅ → ( ¬ 𝑋 = ∪ 𝑛 ↔ ¬ 𝑋 = ∪ ∅ ) ) |
88 |
87
|
biimprcd |
⊢ ( ¬ 𝑋 = ∪ ∅ → ( 𝑛 = ∅ → ¬ 𝑋 = ∪ 𝑛 ) ) |
89 |
88
|
a1dd |
⊢ ( ¬ 𝑋 = ∪ ∅ → ( 𝑛 = ∅ → ( 𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛 ) ) ) |
90 |
84 89
|
syl9r |
⊢ ( ¬ 𝑋 = ∪ ∅ → ( 𝑤 = ∅ → ( 𝑛 ⊆ 𝑤 → ( 𝑛 ∈ Fin → ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
91 |
90
|
com34 |
⊢ ( ¬ 𝑋 = ∪ ∅ → ( 𝑤 = ∅ → ( 𝑛 ∈ Fin → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
92 |
81 91
|
jaod |
⊢ ( ¬ 𝑋 = ∪ ∅ → ( ( ( 𝑤 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ 𝑤 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑤 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ∨ 𝑤 = ∅ ) → ( 𝑛 ∈ Fin → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
93 |
12 92
|
syl5bi |
⊢ ( ¬ 𝑋 = ∪ ∅ → ( 𝑤 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) → ( 𝑛 ∈ Fin → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
94 |
2 93
|
sylan9r |
⊢ ( ( ¬ 𝑋 = ∪ ∅ ∧ 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) → ( 𝑤 ∈ 𝑦 → ( 𝑛 ∈ Fin → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
95 |
94
|
com23 |
⊢ ( ( ¬ 𝑋 = ∪ ∅ ∧ 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) → ( 𝑛 ∈ Fin → ( 𝑤 ∈ 𝑦 → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
96 |
69 95
|
sylan |
⊢ ( ( ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ∧ 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) → ( 𝑛 ∈ Fin → ( 𝑤 ∈ 𝑦 → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
97 |
96
|
ad2ant2lr |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) → ( 𝑛 ∈ Fin → ( 𝑤 ∈ 𝑦 → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) ) |
98 |
97
|
imp |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ 𝑛 ∈ Fin ) → ( 𝑤 ∈ 𝑦 → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) |
99 |
98
|
adantrl |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ( ¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin ) ) → ( 𝑤 ∈ 𝑦 → ( 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) ) |
100 |
99
|
rexlimdv |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ( ¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin ) ) → ( ∃ 𝑤 ∈ 𝑦 𝑛 ⊆ 𝑤 → ¬ 𝑋 = ∪ 𝑛 ) ) |
101 |
61 100
|
syld |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ( ¬ ∪ 𝑦 = ∅ ∧ 𝑛 ∈ Fin ) ) → ( 𝑛 ⊆ ∪ 𝑦 → ¬ 𝑋 = ∪ 𝑛 ) ) |
102 |
101
|
expr |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ¬ ∪ 𝑦 = ∅ ) → ( 𝑛 ∈ Fin → ( 𝑛 ⊆ ∪ 𝑦 → ¬ 𝑋 = ∪ 𝑛 ) ) ) |
103 |
102
|
impcomd |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ¬ ∪ 𝑦 = ∅ ) → ( ( 𝑛 ⊆ ∪ 𝑦 ∧ 𝑛 ∈ Fin ) → ¬ 𝑋 = ∪ 𝑛 ) ) |
104 |
49 103
|
syl5bi |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ¬ ∪ 𝑦 = ∅ ) → ( 𝑛 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) → ¬ 𝑋 = ∪ 𝑛 ) ) |
105 |
104
|
ralrimiv |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ¬ ∪ 𝑦 = ∅ ) → ∀ 𝑛 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ) |
106 |
|
unieq |
⊢ ( 𝑛 = 𝑏 → ∪ 𝑛 = ∪ 𝑏 ) |
107 |
106
|
eqeq2d |
⊢ ( 𝑛 = 𝑏 → ( 𝑋 = ∪ 𝑛 ↔ 𝑋 = ∪ 𝑏 ) ) |
108 |
107
|
notbid |
⊢ ( 𝑛 = 𝑏 → ( ¬ 𝑋 = ∪ 𝑛 ↔ ¬ 𝑋 = ∪ 𝑏 ) ) |
109 |
108
|
cbvralvw |
⊢ ( ∀ 𝑛 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑛 ↔ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) |
110 |
105 109
|
sylib |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ¬ ∪ 𝑦 = ∅ ) → ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) |
111 |
28 48 110
|
jca32 |
⊢ ( ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) ∧ ¬ ∪ 𝑦 = ∅ ) → ( ∪ 𝑦 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ∪ 𝑦 ∧ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
112 |
111
|
ex |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) → ( ¬ ∪ 𝑦 = ∅ → ( ∪ 𝑦 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ∪ 𝑦 ∧ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ) |
113 |
|
orcom |
⊢ ( ( ∪ 𝑦 ∈ { ∅ } ∨ ∪ 𝑦 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ↔ ( ∪ 𝑦 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∨ ∪ 𝑦 ∈ { ∅ } ) ) |
114 |
26
|
elsn |
⊢ ( ∪ 𝑦 ∈ { ∅ } ↔ ∪ 𝑦 = ∅ ) |
115 |
|
sseq2 |
⊢ ( 𝑧 = ∪ 𝑦 → ( 𝑎 ⊆ 𝑧 ↔ 𝑎 ⊆ ∪ 𝑦 ) ) |
116 |
|
pweq |
⊢ ( 𝑧 = ∪ 𝑦 → 𝒫 𝑧 = 𝒫 ∪ 𝑦 ) |
117 |
116
|
ineq1d |
⊢ ( 𝑧 = ∪ 𝑦 → ( 𝒫 𝑧 ∩ Fin ) = ( 𝒫 ∪ 𝑦 ∩ Fin ) ) |
118 |
117
|
raleqdv |
⊢ ( 𝑧 = ∪ 𝑦 → ( ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ↔ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) |
119 |
115 118
|
anbi12d |
⊢ ( 𝑧 = ∪ 𝑦 → ( ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ↔ ( 𝑎 ⊆ ∪ 𝑦 ∧ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
120 |
119
|
elrab |
⊢ ( ∪ 𝑦 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ↔ ( ∪ 𝑦 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ∪ 𝑦 ∧ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) |
121 |
114 120
|
orbi12i |
⊢ ( ( ∪ 𝑦 ∈ { ∅ } ∨ ∪ 𝑦 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ↔ ( ∪ 𝑦 = ∅ ∨ ( ∪ 𝑦 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ∪ 𝑦 ∧ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ) |
122 |
|
df-or |
⊢ ( ( ∪ 𝑦 = ∅ ∨ ( ∪ 𝑦 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ∪ 𝑦 ∧ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ↔ ( ¬ ∪ 𝑦 = ∅ → ( ∪ 𝑦 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ∪ 𝑦 ∧ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ) |
123 |
121 122
|
bitr2i |
⊢ ( ( ¬ ∪ 𝑦 = ∅ → ( ∪ 𝑦 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ∪ 𝑦 ∧ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ↔ ( ∪ 𝑦 ∈ { ∅ } ∨ ∪ 𝑦 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ) ) |
124 |
|
elun |
⊢ ( ∪ 𝑦 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ↔ ( ∪ 𝑦 ∈ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∨ ∪ 𝑦 ∈ { ∅ } ) ) |
125 |
113 123 124
|
3bitr4i |
⊢ ( ( ¬ ∪ 𝑦 = ∅ → ( ∪ 𝑦 ∈ 𝒫 ( fi ‘ 𝑥 ) ∧ ( 𝑎 ⊆ ∪ 𝑦 ∧ ∀ 𝑏 ∈ ( 𝒫 ∪ 𝑦 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ) ) ↔ ∪ 𝑦 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) |
126 |
112 125
|
sylib |
⊢ ( ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) ∧ ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) ) → ∪ 𝑦 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) |
127 |
126
|
ex |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ( ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) ) |
128 |
127
|
alrimiv |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ∀ 𝑦 ( ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) ) |
129 |
|
fvex |
⊢ ( fi ‘ 𝑥 ) ∈ V |
130 |
129
|
pwex |
⊢ 𝒫 ( fi ‘ 𝑥 ) ∈ V |
131 |
130
|
rabex |
⊢ { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∈ V |
132 |
|
p0ex |
⊢ { ∅ } ∈ V |
133 |
131 132
|
unex |
⊢ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∈ V |
134 |
133
|
zorn |
⊢ ( ∀ 𝑦 ( ( 𝑦 ⊆ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∧ [⊊] Or 𝑦 ) → ∪ 𝑦 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ) → ∃ 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 ) |
135 |
128 134
|
syl |
⊢ ( ( ( 𝐽 = ( topGen ‘ ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝑥 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ∧ 𝑎 ∈ 𝒫 ( fi ‘ 𝑥 ) ) ∧ ∀ 𝑏 ∈ ( 𝒫 𝑎 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) → ∃ 𝑢 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ∀ 𝑣 ∈ ( { 𝑧 ∈ 𝒫 ( fi ‘ 𝑥 ) ∣ ( 𝑎 ⊆ 𝑧 ∧ ∀ 𝑏 ∈ ( 𝒫 𝑧 ∩ Fin ) ¬ 𝑋 = ∪ 𝑏 ) } ∪ { ∅ } ) ¬ 𝑢 ⊊ 𝑣 ) |