| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | tgcn.1 | . . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) | 
| 2 |  | tgcn.4 | . . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) | 
| 3 |  | iscn 23244 | . . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽))) | 
| 4 | 1, 2, 3 | syl2anc 584 | . 2
⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽))) | 
| 5 |  | tgcn.3 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 = (topGen‘𝐵)) | 
| 6 |  | topontop 22920 | . . . . . . . . . 10
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) | 
| 7 | 2, 6 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ Top) | 
| 8 | 5, 7 | eqeltrrd 2841 | . . . . . . . 8
⊢ (𝜑 → (topGen‘𝐵) ∈ Top) | 
| 9 |  | tgclb 22978 | . . . . . . . 8
⊢ (𝐵 ∈ TopBases ↔
(topGen‘𝐵) ∈
Top) | 
| 10 | 8, 9 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ TopBases) | 
| 11 |  | bastg 22974 | . . . . . . 7
⊢ (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵)) | 
| 12 | 10, 11 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐵 ⊆ (topGen‘𝐵)) | 
| 13 | 12, 5 | sseqtrrd 4020 | . . . . 5
⊢ (𝜑 → 𝐵 ⊆ 𝐾) | 
| 14 |  | ssralv 4051 | . . . . 5
⊢ (𝐵 ⊆ 𝐾 → (∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) | 
| 15 | 13, 14 | syl 17 | . . . 4
⊢ (𝜑 → (∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) | 
| 16 | 5 | eleq2d 2826 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐾 ↔ 𝑥 ∈ (topGen‘𝐵))) | 
| 17 |  | eltg3 22970 | . . . . . . . . . 10
⊢ (𝐵 ∈ TopBases → (𝑥 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑧))) | 
| 18 | 10, 17 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (topGen‘𝐵) ↔ ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑧))) | 
| 19 | 16, 18 | bitrd 279 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐾 ↔ ∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑧))) | 
| 20 |  | ssralv 4051 | . . . . . . . . . . . 12
⊢ (𝑧 ⊆ 𝐵 → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∀𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽)) | 
| 21 |  | topontop 22920 | . . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) | 
| 22 | 1, 21 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 23 |  | iunopn 22905 | . . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽) → ∪
𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽) | 
| 24 | 23 | ex 412 | . . . . . . . . . . . . 13
⊢ (𝐽 ∈ Top →
(∀𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∪
𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽)) | 
| 25 | 22, 24 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (∀𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∪
𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽)) | 
| 26 | 20, 25 | sylan9r 508 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐵) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∪
𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽)) | 
| 27 |  | imaeq2 6073 | . . . . . . . . . . . . . 14
⊢ (𝑥 = ∪
𝑧 → (◡𝐹 “ 𝑥) = (◡𝐹 “ ∪ 𝑧)) | 
| 28 |  | imauni 7267 | . . . . . . . . . . . . . 14
⊢ (◡𝐹 “ ∪ 𝑧) = ∪ 𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) | 
| 29 | 27, 28 | eqtrdi 2792 | . . . . . . . . . . . . 13
⊢ (𝑥 = ∪
𝑧 → (◡𝐹 “ 𝑥) = ∪ 𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦)) | 
| 30 | 29 | eleq1d 2825 | . . . . . . . . . . . 12
⊢ (𝑥 = ∪
𝑧 → ((◡𝐹 “ 𝑥) ∈ 𝐽 ↔ ∪
𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽)) | 
| 31 | 30 | imbi2d 340 | . . . . . . . . . . 11
⊢ (𝑥 = ∪
𝑧 → ((∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → (◡𝐹 “ 𝑥) ∈ 𝐽) ↔ (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∪
𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽))) | 
| 32 | 26, 31 | syl5ibrcom 247 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ⊆ 𝐵) → (𝑥 = ∪ 𝑧 → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → (◡𝐹 “ 𝑥) ∈ 𝐽))) | 
| 33 | 32 | expimpd 453 | . . . . . . . . 9
⊢ (𝜑 → ((𝑧 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑧) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → (◡𝐹 “ 𝑥) ∈ 𝐽))) | 
| 34 | 33 | exlimdv 1932 | . . . . . . . 8
⊢ (𝜑 → (∃𝑧(𝑧 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑧) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → (◡𝐹 “ 𝑥) ∈ 𝐽))) | 
| 35 | 19, 34 | sylbid 240 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐾 → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → (◡𝐹 “ 𝑥) ∈ 𝐽))) | 
| 36 | 35 | imp 406 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → (◡𝐹 “ 𝑥) ∈ 𝐽)) | 
| 37 | 36 | ralrimdva 3153 | . . . . 5
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)) | 
| 38 |  | imaeq2 6073 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (◡𝐹 “ 𝑥) = (◡𝐹 “ 𝑦)) | 
| 39 | 38 | eleq1d 2825 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((◡𝐹 “ 𝑥) ∈ 𝐽 ↔ (◡𝐹 “ 𝑦) ∈ 𝐽)) | 
| 40 | 39 | cbvralvw 3236 | . . . . 5
⊢
(∀𝑥 ∈
𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽 ↔ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽) | 
| 41 | 37, 40 | imbitrdi 251 | . . . 4
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽)) | 
| 42 | 15, 41 | impbid 212 | . . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽 ↔ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) | 
| 43 | 42 | anbi2d 630 | . 2
⊢ (𝜑 → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐾 (◡𝐹 “ 𝑦) ∈ 𝐽) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽))) | 
| 44 | 4, 43 | bitrd 279 | 1
⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽))) |