| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | alexsubALT.1 | . . 3
⊢ 𝑋 = ∪
𝐽 | 
| 2 | 1 | alexsubALTlem1 24056 | . 2
⊢ (𝐽 ∈ Comp → ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 3 | 1 | alexsubALTlem4 24059 | . . . . 5
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → ∀𝑎 ∈ 𝒫
(fi‘𝑥)(𝑋 = ∪
𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏))) | 
| 4 |  | velpw 4604 | . . . . . . . . 9
⊢ (𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽) | 
| 5 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 = ∪
𝑐 → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐)) | 
| 6 | 5 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ 𝑐)) | 
| 7 |  | eluni 4909 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 ∈ ∪ 𝑐
↔ ∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐)) | 
| 8 |  | ssel 3976 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑐 ⊆ 𝐽 → (𝑤 ∈ 𝑐 → 𝑤 ∈ 𝐽)) | 
| 9 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤 ∈ 𝐽 ↔ 𝑤 ∈ (topGen‘(fi‘𝑥)))) | 
| 10 |  | tg2 22973 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑤 ∈
(topGen‘(fi‘𝑥))
∧ 𝑡 ∈ 𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤)) | 
| 11 | 10 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈
(topGen‘(fi‘𝑥))
→ (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))) | 
| 12 | 9, 11 | biimtrdi 253 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑤 ∈ 𝐽 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤)))) | 
| 13 | 8, 12 | sylan9r 508 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑤 ∈ 𝑐 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤)))) | 
| 14 | 13 | 3impia 1117 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤))) | 
| 15 |  | sseq2 4009 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑧 = 𝑤 → (𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑤)) | 
| 16 | 15 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑤 ∈ 𝑐 ∧ 𝑦 ⊆ 𝑤) → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) | 
| 17 | 16 | ex 412 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑤 ∈ 𝑐 → (𝑦 ⊆ 𝑤 → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)) | 
| 18 | 17 | 3ad2ant3 1135 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑦 ⊆ 𝑤 → ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)) | 
| 19 | 18 | anim2d 612 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → ((𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤) → (𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))) | 
| 20 | 19 | reximdv 3169 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ 𝑦 ⊆ 𝑤) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))) | 
| 21 | 14, 20 | syld 47 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑤 ∈ 𝑐) → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))) | 
| 22 | 21 | 3expia 1121 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑤 ∈ 𝑐 → (𝑡 ∈ 𝑤 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))) | 
| 23 | 22 | com23 86 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑡 ∈ 𝑤 → (𝑤 ∈ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)))) | 
| 24 | 23 | impd 410 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → ((𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))) | 
| 25 | 24 | exlimdv 1932 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (∃𝑤(𝑡 ∈ 𝑤 ∧ 𝑤 ∈ 𝑐) → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))) | 
| 26 | 7, 25 | biimtrid 242 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽) → (𝑡 ∈ ∪ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))) | 
| 27 | 26 | 3adant3 1132 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ ∪ 𝑐 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))) | 
| 28 | 6, 27 | sylbid 240 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 → ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))) | 
| 29 |  | ssel 3976 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑧)) | 
| 30 |  | elunii 4911 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 ∈ 𝑧 ∧ 𝑧 ∈ 𝑐) → 𝑡 ∈ ∪ 𝑐) | 
| 31 | 30 | expcom 413 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ 𝑐 → (𝑡 ∈ 𝑧 → 𝑡 ∈ ∪ 𝑐)) | 
| 32 | 6 | biimprd 248 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ ∪ 𝑐 → 𝑡 ∈ 𝑋)) | 
| 33 | 31, 32 | sylan9r 508 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑧 ∈ 𝑐) → (𝑡 ∈ 𝑧 → 𝑡 ∈ 𝑋)) | 
| 34 | 29, 33 | syl9r 78 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑧 ∈ 𝑐) → (𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋))) | 
| 35 | 34 | rexlimdva 3154 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → (𝑡 ∈ 𝑦 → 𝑡 ∈ 𝑋))) | 
| 36 | 35 | com23 86 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑦 → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 → 𝑡 ∈ 𝑋))) | 
| 37 | 36 | impd 410 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ((𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) → 𝑡 ∈ 𝑋)) | 
| 38 | 37 | rexlimdvw 3159 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧) → 𝑡 ∈ 𝑋)) | 
| 39 | 28, 38 | impbid 212 | . . . . . . . . . . . . . . . 16
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧))) | 
| 40 |  | elunirab 4921 | . . . . . . . . . . . . . . . 16
⊢ (𝑡 ∈ ∪ {𝑦
∈ (fi‘𝑥) ∣
∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ↔ ∃𝑦 ∈ (fi‘𝑥)(𝑡 ∈ 𝑦 ∧ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧)) | 
| 41 | 39, 40 | bitr4di 289 | . . . . . . . . . . . . . . 15
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑡 ∈ 𝑋 ↔ 𝑡 ∈ ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})) | 
| 42 | 41 | eqrdv 2734 | . . . . . . . . . . . . . 14
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → 𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}) | 
| 43 |  | ssrab2 4079 | . . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ⊆ (fi‘𝑥) | 
| 44 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢
(fi‘𝑥) ∈
V | 
| 45 | 44 | elpw2 5333 | . . . . . . . . . . . . . . . 16
⊢ ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥) ↔ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ⊆ (fi‘𝑥)) | 
| 46 | 43, 45 | mpbir 231 | . . . . . . . . . . . . . . 15
⊢ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥) | 
| 47 |  | unieq 4917 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∪ 𝑎 = ∪
{𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}) | 
| 48 | 47 | eqeq2d 2747 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑎 ↔ 𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})) | 
| 49 |  | pweq 4613 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → 𝒫 𝑎 = 𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧}) | 
| 50 | 49 | ineq1d 4218 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝒫 𝑎 ∩ Fin) = (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)) | 
| 51 | 50 | rexeqdv 3326 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏 ↔ ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏)) | 
| 52 | 48, 51 | imbi12d 344 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 = {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ((𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) ↔ (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏))) | 
| 53 | 52 | rspcv 3617 | . . . . . . . . . . . . . . 15
⊢ ({𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∈ 𝒫 (fi‘𝑥) → (∀𝑎 ∈ 𝒫
(fi‘𝑥)(𝑋 = ∪
𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏))) | 
| 54 | 46, 53 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢
(∀𝑎 ∈
𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑋 = ∪ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏)) | 
| 55 | 42, 54 | syl5com 31 | . . . . . . . . . . . . 13
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∀𝑎 ∈ 𝒫
(fi‘𝑥)(𝑋 = ∪
𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏)) | 
| 56 |  | elfpw 9395 | . . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin) ↔ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∧ 𝑏 ∈ Fin)) | 
| 57 |  | ssel 3976 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑡 ∈ 𝑏 → 𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧})) | 
| 58 |  | sseq1 4008 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑡 → (𝑦 ⊆ 𝑧 ↔ 𝑡 ⊆ 𝑧)) | 
| 59 | 58 | rexbidv 3178 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑡 → (∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧 ↔ ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)) | 
| 60 | 59 | elrab 3691 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ↔ (𝑡 ∈ (fi‘𝑥) ∧ ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)) | 
| 61 | 60 | simprbi 496 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 ∈ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧) | 
| 62 | 57, 61 | syl6 35 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑡 ∈ 𝑏 → ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧)) | 
| 63 | 62 | ralrimiv 3144 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧) | 
| 64 |  | sseq2 4009 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = (𝑓‘𝑡) → (𝑡 ⊆ 𝑧 ↔ 𝑡 ⊆ (𝑓‘𝑡))) | 
| 65 | 64 | ac6sfi 9321 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑏 ∈ Fin ∧ ∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧) → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡))) | 
| 66 | 65 | ex 412 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑏 ∈ Fin →
(∀𝑡 ∈ 𝑏 ∃𝑧 ∈ 𝑐 𝑡 ⊆ 𝑧 → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)))) | 
| 67 | 63, 66 | syl5 34 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)))) | 
| 68 | 67 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → ∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)))) | 
| 69 |  | simprll 778 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑓:𝑏⟶𝑐) | 
| 70 |  | frn 6742 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓:𝑏⟶𝑐 → ran 𝑓 ⊆ 𝑐) | 
| 71 | 69, 70 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ⊆ 𝑐) | 
| 72 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑏 ∈ Fin) | 
| 73 |  | ffn 6735 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓:𝑏⟶𝑐 → 𝑓 Fn 𝑏) | 
| 74 |  | dffn4 6825 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑓 Fn 𝑏 ↔ 𝑓:𝑏–onto→ran 𝑓) | 
| 75 | 73, 74 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓:𝑏⟶𝑐 → 𝑓:𝑏–onto→ran 𝑓) | 
| 76 | 75 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → 𝑓:𝑏–onto→ran 𝑓) | 
| 77 | 76 | ad2antrl 728 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑓:𝑏–onto→ran 𝑓) | 
| 78 |  | fodomfi 9351 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑏 ∈ Fin ∧ 𝑓:𝑏–onto→ran 𝑓) → ran 𝑓 ≼ 𝑏) | 
| 79 | 72, 77, 78 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ≼ 𝑏) | 
| 80 |  | domfi 9230 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑏 ∈ Fin ∧ ran 𝑓 ≼ 𝑏) → ran 𝑓 ∈ Fin) | 
| 81 | 72, 79, 80 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ∈ Fin) | 
| 82 | 71, 81 | jca 511 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → (ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin)) | 
| 83 |  | elin 3966 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ran
𝑓 ∈ (𝒫 𝑐 ∩ Fin) ↔ (ran 𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin)) | 
| 84 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ 𝑐 ∈ V | 
| 85 | 84 | elpw2 5333 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ran
𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐) | 
| 86 | 85 | anbi1i 624 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ran
𝑓 ∈ 𝒫 𝑐 ∧ ran 𝑓 ∈ Fin) ↔ (ran 𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin)) | 
| 87 | 83, 86 | bitr2i 276 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ran
𝑓 ⊆ 𝑐 ∧ ran 𝑓 ∈ Fin) ↔ ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin)) | 
| 88 | 82, 87 | sylib 218 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ∈ (𝒫 𝑐 ∩ Fin)) | 
| 89 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 = ∪ 𝑏) | 
| 90 |  | uniiun 5057 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ∪ 𝑏 =
∪ 𝑡 ∈ 𝑏 𝑡 | 
| 91 |  | simprlr 779 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) | 
| 92 |  | ss2iun 5009 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∀𝑡 ∈
𝑏 𝑡 ⊆ (𝑓‘𝑡) → ∪
𝑡 ∈ 𝑏 𝑡 ⊆ ∪
𝑡 ∈ 𝑏 (𝑓‘𝑡)) | 
| 93 | 91, 92 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑡 ∈ 𝑏 𝑡 ⊆ ∪
𝑡 ∈ 𝑏 (𝑓‘𝑡)) | 
| 94 | 90, 93 | eqsstrid 4021 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑏
⊆ ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡)) | 
| 95 |  | fniunfv 7268 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 Fn 𝑏 → ∪
𝑡 ∈ 𝑏 (𝑓‘𝑡) = ∪ ran 𝑓) | 
| 96 | 69, 73, 95 | 3syl 18 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑡 ∈ 𝑏 (𝑓‘𝑡) = ∪ ran 𝑓) | 
| 97 | 94, 96 | sseqtrd 4019 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ 𝑏
⊆ ∪ ran 𝑓) | 
| 98 | 89, 97 | eqsstrd 4017 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 ⊆ ∪ ran
𝑓) | 
| 99 |  | simpll2 1213 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑐 ⊆ 𝐽) | 
| 100 | 71, 99 | sstrd 3993 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ran 𝑓 ⊆ 𝐽) | 
| 101 |  | uniss 4914 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ran
𝑓 ⊆ 𝐽 → ∪ ran
𝑓 ⊆ ∪ 𝐽) | 
| 102 | 101, 1 | sseqtrrdi 4024 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ran
𝑓 ⊆ 𝐽 → ∪ ran
𝑓 ⊆ 𝑋) | 
| 103 | 100, 102 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∪ ran 𝑓 ⊆ 𝑋) | 
| 104 | 98, 103 | eqssd 4000 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → 𝑋 = ∪ ran 𝑓) | 
| 105 |  | unieq 4917 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑑 = ran 𝑓 → ∪ 𝑑 = ∪
ran 𝑓) | 
| 106 | 105 | eqeq2d 2747 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑑 = ran 𝑓 → (𝑋 = ∪ 𝑑 ↔ 𝑋 = ∪ ran 𝑓)) | 
| 107 | 106 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ran
𝑓 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = ∪
ran 𝑓) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) | 
| 108 | 88, 104, 107 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) ∧ ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) ∧ 𝑋 = ∪ 𝑏)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) | 
| 109 | 108 | exp32 420 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → ((𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 110 | 109 | exlimdv 1932 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (∃𝑓(𝑓:𝑏⟶𝑐 ∧ ∀𝑡 ∈ 𝑏 𝑡 ⊆ (𝑓‘𝑡)) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 111 | 68, 110 | syld 47 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) ∧ 𝑏 ∈ Fin) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 112 | 111 | ex 412 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ∈ Fin → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))) | 
| 113 | 112 | com23 86 | . . . . . . . . . . . . . . . 16
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} → (𝑏 ∈ Fin → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))) | 
| 114 | 113 | impd 410 | . . . . . . . . . . . . . . 15
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → ((𝑏 ⊆ {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∧ 𝑏 ∈ Fin) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 115 | 56, 114 | biimtrid 242 | . . . . . . . . . . . . . 14
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin) → (𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 116 | 115 | rexlimdv 3152 | . . . . . . . . . . . . 13
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∃𝑏 ∈ (𝒫 {𝑦 ∈ (fi‘𝑥) ∣ ∃𝑧 ∈ 𝑐 𝑦 ⊆ 𝑧} ∩ Fin)𝑋 = ∪ 𝑏 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) | 
| 117 | 55, 116 | syld 47 | . . . . . . . . . . . 12
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ 𝑐 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑐) → (∀𝑎 ∈ 𝒫
(fi‘𝑥)(𝑋 = ∪
𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) | 
| 118 | 117 | 3exp 1119 | . . . . . . . . . . 11
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑐 ⊆ 𝐽 → (𝑋 = ∪ 𝑐 → (∀𝑎 ∈ 𝒫
(fi‘𝑥)(𝑋 = ∪
𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))) | 
| 119 | 118 | com34 91 | . . . . . . . . . 10
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝑐 ⊆ 𝐽 → (∀𝑎 ∈ 𝒫 (fi‘𝑥)(𝑋 = ∪ 𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))) | 
| 120 | 119 | com23 86 | . . . . . . . . 9
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫
(fi‘𝑥)(𝑋 = ∪
𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑐 ⊆ 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))) | 
| 121 | 4, 120 | syl7bi 255 | . . . . . . . 8
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫
(fi‘𝑥)(𝑋 = ∪
𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))) | 
| 122 | 121 | ralrimdv 3151 | . . . . . . 7
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫
(fi‘𝑥)(𝑋 = ∪
𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 123 |  | fibas 22985 | . . . . . . . . 9
⊢
(fi‘𝑥) ∈
TopBases | 
| 124 |  | tgcl 22977 | . . . . . . . . 9
⊢
((fi‘𝑥) ∈
TopBases → (topGen‘(fi‘𝑥)) ∈ Top) | 
| 125 | 123, 124 | ax-mp 5 | . . . . . . . 8
⊢
(topGen‘(fi‘𝑥)) ∈ Top | 
| 126 |  | eleq1 2828 | . . . . . . . 8
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (𝐽 ∈ Top ↔
(topGen‘(fi‘𝑥))
∈ Top)) | 
| 127 | 125, 126 | mpbiri 258 | . . . . . . 7
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → 𝐽 ∈ Top) | 
| 128 | 122, 127 | jctild 525 | . . . . . 6
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫
(fi‘𝑥)(𝑋 = ∪
𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)))) | 
| 129 | 1 | iscmp 23397 | . . . . . 6
⊢ (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) | 
| 130 | 128, 129 | imbitrrdi 252 | . . . . 5
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑎 ∈ 𝒫
(fi‘𝑥)(𝑋 = ∪
𝑎 → ∃𝑏 ∈ (𝒫 𝑎 ∩ Fin)𝑋 = ∪ 𝑏) → 𝐽 ∈ Comp)) | 
| 131 | 3, 130 | syld 47 | . . . 4
⊢ (𝐽 = (topGen‘(fi‘𝑥)) → (∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑) → 𝐽 ∈ Comp)) | 
| 132 | 131 | imp 406 | . . 3
⊢ ((𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp) | 
| 133 | 132 | exlimiv 1929 | . 2
⊢
(∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑)) → 𝐽 ∈ Comp) | 
| 134 | 2, 133 | impbii 209 | 1
⊢ (𝐽 ∈ Comp ↔ ∃𝑥(𝐽 = (topGen‘(fi‘𝑥)) ∧ ∀𝑐 ∈ 𝒫 𝑥(𝑋 = ∪ 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = ∪ 𝑑))) |