Step |
Hyp |
Ref |
Expression |
1 |
|
alexsub.1 |
⊢ ( 𝜑 → 𝑋 ∈ UFL ) |
2 |
|
alexsub.2 |
⊢ ( 𝜑 → 𝑋 = ∪ 𝐵 ) |
3 |
|
alexsub.3 |
⊢ ( 𝜑 → 𝐽 = ( topGen ‘ ( fi ‘ 𝐵 ) ) ) |
4 |
|
alexsub.4 |
⊢ ( ( 𝜑 ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 ) |
5 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝑋 ∈ UFL ) |
6 |
2
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝑋 = ∪ 𝐵 ) |
7 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝐽 = ( topGen ‘ ( fi ‘ 𝐵 ) ) ) |
8 |
4
|
adantlr |
⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) ∧ ( 𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝑥 ∩ Fin ) 𝑋 = ∪ 𝑦 ) |
9 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → 𝑓 ∈ ( UFil ‘ 𝑋 ) ) |
10 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → ( 𝐽 fLim 𝑓 ) = ∅ ) |
11 |
5 6 7 8 9 10
|
alexsublem |
⊢ ¬ ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) |
12 |
11
|
pm2.21i |
⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( UFil ‘ 𝑋 ) ∧ ( 𝐽 fLim 𝑓 ) = ∅ ) ) → ¬ ( 𝐽 fLim 𝑓 ) = ∅ ) |
13 |
12
|
expr |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( ( 𝐽 fLim 𝑓 ) = ∅ → ¬ ( 𝐽 fLim 𝑓 ) = ∅ ) ) |
14 |
13
|
pm2.01d |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ¬ ( 𝐽 fLim 𝑓 ) = ∅ ) |
15 |
14
|
neqned |
⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( UFil ‘ 𝑋 ) ) → ( 𝐽 fLim 𝑓 ) ≠ ∅ ) |
16 |
15
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) |
17 |
|
fibas |
⊢ ( fi ‘ 𝐵 ) ∈ TopBases |
18 |
|
tgtopon |
⊢ ( ( fi ‘ 𝐵 ) ∈ TopBases → ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) ) |
19 |
17 18
|
ax-mp |
⊢ ( topGen ‘ ( fi ‘ 𝐵 ) ) ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) |
20 |
3 19
|
eqeltrdi |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) ) |
21 |
1
|
elexd |
⊢ ( 𝜑 → 𝑋 ∈ V ) |
22 |
2 21
|
eqeltrrd |
⊢ ( 𝜑 → ∪ 𝐵 ∈ V ) |
23 |
|
uniexb |
⊢ ( 𝐵 ∈ V ↔ ∪ 𝐵 ∈ V ) |
24 |
22 23
|
sylibr |
⊢ ( 𝜑 → 𝐵 ∈ V ) |
25 |
|
fiuni |
⊢ ( 𝐵 ∈ V → ∪ 𝐵 = ∪ ( fi ‘ 𝐵 ) ) |
26 |
24 25
|
syl |
⊢ ( 𝜑 → ∪ 𝐵 = ∪ ( fi ‘ 𝐵 ) ) |
27 |
2 26
|
eqtrd |
⊢ ( 𝜑 → 𝑋 = ∪ ( fi ‘ 𝐵 ) ) |
28 |
27
|
fveq2d |
⊢ ( 𝜑 → ( TopOn ‘ 𝑋 ) = ( TopOn ‘ ∪ ( fi ‘ 𝐵 ) ) ) |
29 |
20 28
|
eleqtrrd |
⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
30 |
|
ufilcmp |
⊢ ( ( 𝑋 ∈ UFL ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ∈ Comp ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) ) |
31 |
1 29 30
|
syl2anc |
⊢ ( 𝜑 → ( 𝐽 ∈ Comp ↔ ∀ 𝑓 ∈ ( UFil ‘ 𝑋 ) ( 𝐽 fLim 𝑓 ) ≠ ∅ ) ) |
32 |
16 31
|
mpbird |
⊢ ( 𝜑 → 𝐽 ∈ Comp ) |