| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hauscmplem.3 | . . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Haus) | 
| 2 |  | haustop 23340 | . . . . . . 7
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) | 
| 3 | 1, 2 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐽 ∈ Top) | 
| 4 | 3 | ad3antrrr 730 | . . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝐽 ∈ Top) | 
| 5 |  | hauscmp.1 | . . . . . 6
⊢ 𝑋 = ∪
𝐽 | 
| 6 | 5 | topopn 22913 | . . . . 5
⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) | 
| 7 | 4, 6 | syl 17 | . . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑋 ∈ 𝐽) | 
| 8 |  | hauscmplem.6 | . . . . . 6
⊢ (𝜑 → 𝐴 ∈ (𝑋 ∖ 𝑆)) | 
| 9 | 8 | eldifad 3962 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑋) | 
| 10 | 9 | ad3antrrr 730 | . . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝐴 ∈ 𝑋) | 
| 11 | 5 | clstop 23078 | . . . . . . 7
⊢ (𝐽 ∈ Top →
((cls‘𝐽)‘𝑋) = 𝑋) | 
| 12 | 4, 11 | syl 17 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = 𝑋) | 
| 13 |  | simplr 768 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∪ 𝑥) | 
| 14 |  | unieq 4917 | . . . . . . . . . . . 12
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∪ ∅) | 
| 15 |  | uni0 4934 | . . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ | 
| 16 | 14, 15 | eqtrdi 2792 | . . . . . . . . . . 11
⊢ (𝑥 = ∅ → ∪ 𝑥 =
∅) | 
| 17 | 16 | adantl 481 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ∪ 𝑥 =
∅) | 
| 18 | 13, 17 | sseqtrd 4019 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 ⊆ ∅) | 
| 19 |  | ss0 4401 | . . . . . . . . 9
⊢ (𝑆 ⊆ ∅ → 𝑆 = ∅) | 
| 20 | 18, 19 | syl 17 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → 𝑆 = ∅) | 
| 21 | 20 | difeq2d 4125 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → (𝑋 ∖ 𝑆) = (𝑋 ∖ ∅)) | 
| 22 |  | dif0 4377 | . . . . . . 7
⊢ (𝑋 ∖ ∅) = 𝑋 | 
| 23 | 21, 22 | eqtrdi 2792 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → (𝑋 ∖ 𝑆) = 𝑋) | 
| 24 | 12, 23 | eqtr4d 2779 | . . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) = (𝑋 ∖ 𝑆)) | 
| 25 |  | eqimss 4041 | . . . . 5
⊢
(((cls‘𝐽)‘𝑋) = (𝑋 ∖ 𝑆) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆)) | 
| 26 | 24, 25 | syl 17 | . . . 4
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆)) | 
| 27 |  | eleq2 2829 | . . . . . 6
⊢ (𝑧 = 𝑋 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑋)) | 
| 28 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑧 = 𝑋 → ((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘𝑋)) | 
| 29 | 28 | sseq1d 4014 | . . . . . 6
⊢ (𝑧 = 𝑋 → (((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆) ↔ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))) | 
| 30 | 27, 29 | anbi12d 632 | . . . . 5
⊢ (𝑧 = 𝑋 → ((𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)) ↔ (𝐴 ∈ 𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆)))) | 
| 31 | 30 | rspcev 3621 | . . . 4
⊢ ((𝑋 ∈ 𝐽 ∧ (𝐴 ∈ 𝑋 ∧ ((cls‘𝐽)‘𝑋) ⊆ (𝑋 ∖ 𝑆))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆))) | 
| 32 | 7, 10, 26, 31 | syl12anc 836 | . . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 = ∅) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆))) | 
| 33 |  | elin 3966 | . . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) ↔ (𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin)) | 
| 34 |  | id 22 | . . . . . . . 8
⊢ (𝑥 ∈ Fin → 𝑥 ∈ Fin) | 
| 35 |  | elpwi 4606 | . . . . . . . . . . 11
⊢ (𝑥 ∈ 𝒫 𝑂 → 𝑥 ⊆ 𝑂) | 
| 36 | 35 | sseld 3981 | . . . . . . . . . 10
⊢ (𝑥 ∈ 𝒫 𝑂 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑂)) | 
| 37 |  | difeq2 4119 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → (𝑋 ∖ 𝑦) = (𝑋 ∖ 𝑧)) | 
| 38 | 37 | sseq2d 4015 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → (((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦) ↔ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))) | 
| 39 | 38 | anbi2d 630 | . . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → ((𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) ↔ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))) | 
| 40 | 39 | rexbidv 3178 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) ↔ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))) | 
| 41 |  | hauscmplem.2 | . . . . . . . . . . . 12
⊢ 𝑂 = {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))} | 
| 42 | 40, 41 | elrab2 3694 | . . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑂 ↔ (𝑧 ∈ 𝐽 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))) | 
| 43 | 42 | simprbi 496 | . . . . . . . . . 10
⊢ (𝑧 ∈ 𝑂 → ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))) | 
| 44 | 36, 43 | syl6 35 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝒫 𝑂 → (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)))) | 
| 45 | 44 | ralrimiv 3144 | . . . . . . . 8
⊢ (𝑥 ∈ 𝒫 𝑂 → ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))) | 
| 46 |  | eleq2 2829 | . . . . . . . . . 10
⊢ (𝑤 = (𝑓‘𝑧) → (𝐴 ∈ 𝑤 ↔ 𝐴 ∈ (𝑓‘𝑧))) | 
| 47 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑤 = (𝑓‘𝑧) → ((cls‘𝐽)‘𝑤) = ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 48 | 47 | sseq1d 4014 | . . . . . . . . . 10
⊢ (𝑤 = (𝑓‘𝑧) → (((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧) ↔ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) | 
| 49 | 46, 48 | anbi12d 632 | . . . . . . . . 9
⊢ (𝑤 = (𝑓‘𝑧) → ((𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧)) ↔ (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) | 
| 50 | 49 | ac6sfi 9321 | . . . . . . . 8
⊢ ((𝑥 ∈ Fin ∧ ∀𝑧 ∈ 𝑥 ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑧))) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) | 
| 51 | 34, 45, 50 | syl2anr 597 | . . . . . . 7
⊢ ((𝑥 ∈ 𝒫 𝑂 ∧ 𝑥 ∈ Fin) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) | 
| 52 | 33, 51 | sylbi 217 | . . . . . 6
⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) | 
| 53 | 52 | ad2antlr 727 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → ∃𝑓(𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) | 
| 54 | 3 | ad3antrrr 730 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐽 ∈ Top) | 
| 55 |  | frn 6742 | . . . . . . . 8
⊢ (𝑓:𝑥⟶𝐽 → ran 𝑓 ⊆ 𝐽) | 
| 56 | 55 | ad2antrl 728 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ⊆ 𝐽) | 
| 57 |  | simprr 772 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → 𝑥 ≠ ∅) | 
| 58 |  | simpl 482 | . . . . . . . 8
⊢ ((𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) → 𝑓:𝑥⟶𝐽) | 
| 59 |  | fdm 6744 | . . . . . . . . . . . 12
⊢ (𝑓:𝑥⟶𝐽 → dom 𝑓 = 𝑥) | 
| 60 | 59 | eqeq1d 2738 | . . . . . . . . . . 11
⊢ (𝑓:𝑥⟶𝐽 → (dom 𝑓 = ∅ ↔ 𝑥 = ∅)) | 
| 61 |  | dm0rn0 5934 | . . . . . . . . . . 11
⊢ (dom
𝑓 = ∅ ↔ ran
𝑓 =
∅) | 
| 62 | 60, 61 | bitr3di 286 | . . . . . . . . . 10
⊢ (𝑓:𝑥⟶𝐽 → (𝑥 = ∅ ↔ ran 𝑓 = ∅)) | 
| 63 | 62 | necon3bid 2984 | . . . . . . . . 9
⊢ (𝑓:𝑥⟶𝐽 → (𝑥 ≠ ∅ ↔ ran 𝑓 ≠ ∅)) | 
| 64 | 63 | biimpac 478 | . . . . . . . 8
⊢ ((𝑥 ≠ ∅ ∧ 𝑓:𝑥⟶𝐽) → ran 𝑓 ≠ ∅) | 
| 65 | 57, 58, 64 | syl2an 596 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ≠ ∅) | 
| 66 | 33 | simprbi 496 | . . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝑂 ∩ Fin) → 𝑥 ∈ Fin) | 
| 67 | 66 | ad2antlr 727 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → 𝑥 ∈ Fin) | 
| 68 |  | ffn 6735 | . . . . . . . . . 10
⊢ (𝑓:𝑥⟶𝐽 → 𝑓 Fn 𝑥) | 
| 69 |  | dffn4 6825 | . . . . . . . . . 10
⊢ (𝑓 Fn 𝑥 ↔ 𝑓:𝑥–onto→ran 𝑓) | 
| 70 | 68, 69 | sylib 218 | . . . . . . . . 9
⊢ (𝑓:𝑥⟶𝐽 → 𝑓:𝑥–onto→ran 𝑓) | 
| 71 | 70 | adantr 480 | . . . . . . . 8
⊢ ((𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧))) → 𝑓:𝑥–onto→ran 𝑓) | 
| 72 |  | fofi 9352 | . . . . . . . 8
⊢ ((𝑥 ∈ Fin ∧ 𝑓:𝑥–onto→ran 𝑓) → ran 𝑓 ∈ Fin) | 
| 73 | 67, 71, 72 | syl2an 596 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ran 𝑓 ∈ Fin) | 
| 74 |  | fiinopn 22908 | . . . . . . . 8
⊢ (𝐽 ∈ Top → ((ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin) → ∩ ran 𝑓 ∈ 𝐽)) | 
| 75 | 74 | imp 406 | . . . . . . 7
⊢ ((𝐽 ∈ Top ∧ (ran 𝑓 ⊆ 𝐽 ∧ ran 𝑓 ≠ ∅ ∧ ran 𝑓 ∈ Fin)) → ∩ ran 𝑓 ∈ 𝐽) | 
| 76 | 54, 56, 65, 73, 75 | syl13anc 1373 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran
𝑓 ∈ 𝐽) | 
| 77 |  | simpl 482 | . . . . . . . . . 10
⊢ ((𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → 𝐴 ∈ (𝑓‘𝑧)) | 
| 78 | 77 | ralimi 3082 | . . . . . . . . 9
⊢
(∀𝑧 ∈
𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧)) | 
| 79 | 78 | ad2antll 729 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧)) | 
| 80 | 8 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ (𝑋 ∖ 𝑆)) | 
| 81 |  | eliin 4995 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝑋 ∖ 𝑆) → (𝐴 ∈ ∩
𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧))) | 
| 82 | 80, 81 | syl 17 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → (𝐴 ∈ ∩
𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝐴 ∈ (𝑓‘𝑧))) | 
| 83 | 79, 82 | mpbird 257 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ ∩
𝑧 ∈ 𝑥 (𝑓‘𝑧)) | 
| 84 | 68 | ad2antrl 728 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑓 Fn 𝑥) | 
| 85 |  | fnrnfv 6967 | . . . . . . . . . 10
⊢ (𝑓 Fn 𝑥 → ran 𝑓 = {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)}) | 
| 86 | 85 | inteqd 4950 | . . . . . . . . 9
⊢ (𝑓 Fn 𝑥 → ∩ ran
𝑓 = ∩ {𝑦
∣ ∃𝑧 ∈
𝑥 𝑦 = (𝑓‘𝑧)}) | 
| 87 |  | fvex 6918 | . . . . . . . . . 10
⊢ (𝑓‘𝑧) ∈ V | 
| 88 | 87 | dfiin2 5033 | . . . . . . . . 9
⊢ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) = ∩ {𝑦 ∣ ∃𝑧 ∈ 𝑥 𝑦 = (𝑓‘𝑧)} | 
| 89 | 86, 88 | eqtr4di 2794 | . . . . . . . 8
⊢ (𝑓 Fn 𝑥 → ∩ ran
𝑓 = ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧)) | 
| 90 | 84, 89 | syl 17 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran
𝑓 = ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧)) | 
| 91 | 83, 90 | eleqtrrd 2843 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝐴 ∈ ∩ ran
𝑓) | 
| 92 | 57 | adantr 480 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑥 ≠ ∅) | 
| 93 | 3 | ad4antr 732 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥
∧ 𝑥 ≠ ∅))
∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → 𝐽 ∈ Top) | 
| 94 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . 15
⊢ ((𝑓:𝑥⟶𝐽 ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ 𝐽) | 
| 95 | 94 | adantll 714 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥
∧ 𝑥 ≠ ∅))
∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ∈ 𝐽) | 
| 96 |  | elssuni 4936 | . . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑧) ∈ 𝐽 → (𝑓‘𝑧) ⊆ ∪ 𝐽) | 
| 97 | 95, 96 | syl 17 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥
∧ 𝑥 ≠ ∅))
∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ ∪ 𝐽) | 
| 98 | 97, 5 | sseqtrrdi 4024 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥
∧ 𝑥 ≠ ∅))
∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ 𝑋) | 
| 99 | 5 | clscld 23056 | . . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ (𝑓‘𝑧) ⊆ 𝑋) → ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) | 
| 100 | 93, 98, 99 | syl2anc 584 | . . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥
∧ 𝑥 ≠ ∅))
∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) | 
| 101 | 100 | ralrimiva 3145 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) | 
| 102 | 101 | adantrr 717 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) | 
| 103 |  | iincld 23048 | . . . . . . . . 9
⊢ ((𝑥 ≠ ∅ ∧
∀𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) | 
| 104 | 92, 102, 103 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽)) | 
| 105 | 5 | sscls 23065 | . . . . . . . . . . . . 13
⊢ ((𝐽 ∈ Top ∧ (𝑓‘𝑧) ⊆ 𝑋) → (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 106 | 93, 98, 105 | syl2anc 584 | . . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥
∧ 𝑥 ≠ ∅))
∧ 𝑓:𝑥⟶𝐽) ∧ 𝑧 ∈ 𝑥) → (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 107 | 106 | ralrimiva 3145 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∀𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 108 |  | ssel 3976 | . . . . . . . . . . . . . 14
⊢ ((𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (𝑦 ∈ (𝑓‘𝑧) → 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)))) | 
| 109 | 108 | ral2imi 3084 | . . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧) → ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)))) | 
| 110 |  | eliin 4995 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧))) | 
| 111 | 110 | elv 3484 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑓‘𝑧)) | 
| 112 |  | eliin 4995 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)))) | 
| 113 | 112 | elv 3484 | . . . . . . . . . . . . 13
⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 114 | 109, 111,
113 | 3imtr4g 296 | . . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → (𝑦 ∈ ∩
𝑧 ∈ 𝑥 (𝑓‘𝑧) → 𝑦 ∈ ∩
𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)))) | 
| 115 | 114 | ssrdv 3988 | . . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝑥 (𝑓‘𝑧) ⊆ ((cls‘𝐽)‘(𝑓‘𝑧)) → ∩
𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩
𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 116 | 107, 115 | syl 17 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ 𝑓:𝑥⟶𝐽) → ∩
𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩
𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 117 | 116 | adantrr 717 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑓‘𝑧) ⊆ ∩
𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 118 | 90, 117 | eqsstrd 4017 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ ran
𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 119 | 5 | clsss2 23081 | . . . . . . . 8
⊢
((∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ∈ (Clsd‘𝐽) ∧ ∩ ran
𝑓 ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) → ((cls‘𝐽)‘∩ ran
𝑓) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 120 | 104, 118,
119 | syl2anc 584 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ((cls‘𝐽)‘∩ ran
𝑓) ⊆ ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧))) | 
| 121 |  | ssel 3976 | . . . . . . . . . . . . 13
⊢
(((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ (𝑋 ∖ 𝑧))) | 
| 122 | 121 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ (𝑋 ∖ 𝑧))) | 
| 123 | 122 | ral2imi 3084 | . . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (∀𝑧 ∈ 𝑥 𝑦 ∈ ((cls‘𝐽)‘(𝑓‘𝑧)) → ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧))) | 
| 124 |  | eliin 4995 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧))) | 
| 125 | 124 | elv 3484 | . . . . . . . . . . 11
⊢ (𝑦 ∈ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ↔ ∀𝑧 ∈ 𝑥 𝑦 ∈ (𝑋 ∖ 𝑧)) | 
| 126 | 123, 113,
125 | 3imtr4g 296 | . . . . . . . . . 10
⊢
(∀𝑧 ∈
𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → (𝑦 ∈ ∩
𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) → 𝑦 ∈ ∩
𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧))) | 
| 127 | 126 | ssrdv 3988 | . . . . . . . . 9
⊢
(∀𝑧 ∈
𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)) → ∩
𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧)) | 
| 128 | 127 | ad2antll 729 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧)) | 
| 129 |  | iindif2 5076 | . . . . . . . . . 10
⊢ (𝑥 ≠ ∅ → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) = (𝑋 ∖ ∪
𝑧 ∈ 𝑥 𝑧)) | 
| 130 | 92, 129 | syl 17 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) = (𝑋 ∖ ∪
𝑧 ∈ 𝑥 𝑧)) | 
| 131 |  | simplrl 776 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → 𝑆 ⊆ ∪ 𝑥) | 
| 132 |  | uniiun 5057 | . . . . . . . . . . . 12
⊢ ∪ 𝑥 =
∪ 𝑧 ∈ 𝑥 𝑧 | 
| 133 | 132 | sseq2i 4012 | . . . . . . . . . . 11
⊢ (𝑆 ⊆ ∪ 𝑥
↔ 𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧) | 
| 134 |  | sscon 4142 | . . . . . . . . . . 11
⊢ (𝑆 ⊆ ∪ 𝑧 ∈ 𝑥 𝑧 → (𝑋 ∖ ∪
𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆)) | 
| 135 | 133, 134 | sylbi 217 | . . . . . . . . . 10
⊢ (𝑆 ⊆ ∪ 𝑥
→ (𝑋 ∖ ∪ 𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆)) | 
| 136 | 131, 135 | syl 17 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → (𝑋 ∖ ∪
𝑧 ∈ 𝑥 𝑧) ⊆ (𝑋 ∖ 𝑆)) | 
| 137 | 130, 136 | eqsstrd 4017 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 (𝑋 ∖ 𝑧) ⊆ (𝑋 ∖ 𝑆)) | 
| 138 | 128, 137 | sstrd 3993 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∩ 𝑧 ∈ 𝑥 ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑆)) | 
| 139 | 120, 138 | sstrd 3993 | . . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ((cls‘𝐽)‘∩ ran
𝑓) ⊆ (𝑋 ∖ 𝑆)) | 
| 140 |  | eleq2 2829 | . . . . . . . 8
⊢ (𝑧 = ∩
ran 𝑓 → (𝐴 ∈ 𝑧 ↔ 𝐴 ∈ ∩ ran
𝑓)) | 
| 141 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑧 = ∩
ran 𝑓 →
((cls‘𝐽)‘𝑧) = ((cls‘𝐽)‘∩ ran 𝑓)) | 
| 142 | 141 | sseq1d 4014 | . . . . . . . 8
⊢ (𝑧 = ∩
ran 𝑓 →
(((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆) ↔ ((cls‘𝐽)‘∩ ran
𝑓) ⊆ (𝑋 ∖ 𝑆))) | 
| 143 | 140, 142 | anbi12d 632 | . . . . . . 7
⊢ (𝑧 = ∩
ran 𝑓 → ((𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆)) ↔ (𝐴 ∈ ∩ ran
𝑓 ∧ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆)))) | 
| 144 | 143 | rspcev 3621 | . . . . . 6
⊢ ((∩ ran 𝑓 ∈ 𝐽 ∧ (𝐴 ∈ ∩ ran
𝑓 ∧ ((cls‘𝐽)‘∩ ran 𝑓) ⊆ (𝑋 ∖ 𝑆))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆))) | 
| 145 | 76, 91, 139, 144 | syl12anc 836 | . . . . 5
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) ∧ (𝑓:𝑥⟶𝐽 ∧ ∀𝑧 ∈ 𝑥 (𝐴 ∈ (𝑓‘𝑧) ∧ ((cls‘𝐽)‘(𝑓‘𝑧)) ⊆ (𝑋 ∖ 𝑧)))) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆))) | 
| 146 | 53, 145 | exlimddv 1934 | . . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ (𝑆 ⊆ ∪ 𝑥 ∧ 𝑥 ≠ ∅)) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆))) | 
| 147 | 146 | anassrs 467 | . . 3
⊢ ((((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆))) | 
| 148 | 32, 147 | pm2.61dane 3028 | . 2
⊢ (((𝜑 ∧ 𝑥 ∈ (𝒫 𝑂 ∩ Fin)) ∧ 𝑆 ⊆ ∪ 𝑥) → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆))) | 
| 149 | 1 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ Haus) | 
| 150 |  | hauscmplem.4 | . . . . . . . . 9
⊢ (𝜑 → 𝑆 ⊆ 𝑋) | 
| 151 | 150 | sselda 3982 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑋) | 
| 152 | 9 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐴 ∈ 𝑋) | 
| 153 |  | id 22 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝑆 → 𝑥 ∈ 𝑆) | 
| 154 | 8 | eldifbd 3963 | . . . . . . . . 9
⊢ (𝜑 → ¬ 𝐴 ∈ 𝑆) | 
| 155 |  | nelne2 3039 | . . . . . . . . 9
⊢ ((𝑥 ∈ 𝑆 ∧ ¬ 𝐴 ∈ 𝑆) → 𝑥 ≠ 𝐴) | 
| 156 | 153, 154,
155 | syl2anr 597 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ≠ 𝐴) | 
| 157 | 5 | hausnei 23337 | . . . . . . . 8
⊢ ((𝐽 ∈ Haus ∧ (𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑥 ≠ 𝐴)) → ∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)) | 
| 158 | 149, 151,
152, 156, 157 | syl13anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)) | 
| 159 |  | 3anass 1094 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) ↔ (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅))) | 
| 160 |  | elssuni 4936 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ ∪ 𝐽) | 
| 161 | 160, 5 | sseqtrrdi 4024 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ 𝐽 → 𝑤 ⊆ 𝑋) | 
| 162 | 161 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → 𝑤 ⊆ 𝑋) | 
| 163 |  | incom 4208 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∩ 𝑤) = (𝑤 ∩ 𝑦) | 
| 164 | 163 | eqeq1i 2741 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∩ 𝑤) = ∅ ↔ (𝑤 ∩ 𝑦) = ∅) | 
| 165 |  | reldisj 4452 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 ⊆ 𝑋 → ((𝑤 ∩ 𝑦) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦))) | 
| 166 | 164, 165 | bitrid 283 | . . . . . . . . . . . . . . 15
⊢ (𝑤 ⊆ 𝑋 → ((𝑦 ∩ 𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦))) | 
| 167 | 162, 166 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑦 ∩ 𝑤) = ∅ ↔ 𝑤 ⊆ (𝑋 ∖ 𝑦))) | 
| 168 | 149, 2 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐽 ∈ Top) | 
| 169 | 5 | opncld 23042 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽)) | 
| 170 | 168, 169 | sylan 580 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽)) | 
| 171 | 170 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽)) | 
| 172 | 5 | clsss2 23081 | . . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽) ∧ 𝑤 ⊆ (𝑋 ∖ 𝑦)) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)) | 
| 173 | 172 | ex 412 | . . . . . . . . . . . . . . 15
⊢ ((𝑋 ∖ 𝑦) ∈ (Clsd‘𝐽) → (𝑤 ⊆ (𝑋 ∖ 𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))) | 
| 174 | 171, 173 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → (𝑤 ⊆ (𝑋 ∖ 𝑦) → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))) | 
| 175 | 167, 174 | sylbid 240 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑦 ∩ 𝑤) = ∅ → ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))) | 
| 176 | 175 | anim2d 612 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))) | 
| 177 | 176 | anim2d 612 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅)) → (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))) | 
| 178 | 159, 177 | biimtrid 242 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) ∧ 𝑤 ∈ 𝐽) → ((𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))) | 
| 179 | 178 | reximdva 3167 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))) | 
| 180 |  | r19.42v 3190 | . . . . . . . . 9
⊢
(∃𝑤 ∈
𝐽 (𝑥 ∈ 𝑦 ∧ (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))) ↔ (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))) | 
| 181 | 179, 180 | imbitrdi 251 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑦 ∈ 𝐽) → (∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))) | 
| 182 | 181 | reximdva 3167 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∃𝑦 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ 𝐴 ∈ 𝑤 ∧ (𝑦 ∩ 𝑤) = ∅) → ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))))) | 
| 183 | 158, 182 | mpd 15 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))) | 
| 184 | 41 | unieqi 4918 | . . . . . . . 8
⊢ ∪ 𝑂 =
∪ {𝑦 ∈ 𝐽 ∣ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))} | 
| 185 | 184 | eleq2i 2832 | . . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑂
↔ 𝑥 ∈ ∪ {𝑦
∈ 𝐽 ∣
∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))}) | 
| 186 |  | elunirab 4921 | . . . . . . 7
⊢ (𝑥 ∈ ∪ {𝑦
∈ 𝐽 ∣
∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦))} ↔ ∃𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))) | 
| 187 | 185, 186 | bitri 275 | . . . . . 6
⊢ (𝑥 ∈ ∪ 𝑂
↔ ∃𝑦 ∈
𝐽 (𝑥 ∈ 𝑦 ∧ ∃𝑤 ∈ 𝐽 (𝐴 ∈ 𝑤 ∧ ((cls‘𝐽)‘𝑤) ⊆ (𝑋 ∖ 𝑦)))) | 
| 188 | 183, 187 | sylibr 234 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ ∪ 𝑂) | 
| 189 | 188 | ex 412 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ ∪ 𝑂)) | 
| 190 | 189 | ssrdv 3988 | . . 3
⊢ (𝜑 → 𝑆 ⊆ ∪ 𝑂) | 
| 191 |  | unieq 4917 | . . . . . 6
⊢ (𝑧 = 𝑂 → ∪ 𝑧 = ∪
𝑂) | 
| 192 | 191 | sseq2d 4015 | . . . . 5
⊢ (𝑧 = 𝑂 → (𝑆 ⊆ ∪ 𝑧 ↔ 𝑆 ⊆ ∪ 𝑂)) | 
| 193 |  | pweq 4613 | . . . . . . 7
⊢ (𝑧 = 𝑂 → 𝒫 𝑧 = 𝒫 𝑂) | 
| 194 | 193 | ineq1d 4218 | . . . . . 6
⊢ (𝑧 = 𝑂 → (𝒫 𝑧 ∩ Fin) = (𝒫 𝑂 ∩ Fin)) | 
| 195 | 194 | rexeqdv 3326 | . . . . 5
⊢ (𝑧 = 𝑂 → (∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥 ↔ ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥)) | 
| 196 | 192, 195 | imbi12d 344 | . . . 4
⊢ (𝑧 = 𝑂 → ((𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥) ↔ (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥))) | 
| 197 |  | hauscmplem.5 | . . . . 5
⊢ (𝜑 → (𝐽 ↾t 𝑆) ∈ Comp) | 
| 198 | 5 | cmpsub 23409 | . . . . . 6
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Comp ↔ ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥))) | 
| 199 | 198 | biimp3a 1470 | . . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ (𝐽 ↾t 𝑆) ∈ Comp) → ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥)) | 
| 200 | 3, 150, 197, 199 | syl3anc 1372 | . . . 4
⊢ (𝜑 → ∀𝑧 ∈ 𝒫 𝐽(𝑆 ⊆ ∪ 𝑧 → ∃𝑥 ∈ (𝒫 𝑧 ∩ Fin)𝑆 ⊆ ∪ 𝑥)) | 
| 201 | 41 | ssrab3 4081 | . . . . 5
⊢ 𝑂 ⊆ 𝐽 | 
| 202 |  | elpw2g 5332 | . . . . . 6
⊢ (𝐽 ∈ Haus → (𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽)) | 
| 203 | 1, 202 | syl 17 | . . . . 5
⊢ (𝜑 → (𝑂 ∈ 𝒫 𝐽 ↔ 𝑂 ⊆ 𝐽)) | 
| 204 | 201, 203 | mpbiri 258 | . . . 4
⊢ (𝜑 → 𝑂 ∈ 𝒫 𝐽) | 
| 205 | 196, 200,
204 | rspcdva 3622 | . . 3
⊢ (𝜑 → (𝑆 ⊆ ∪ 𝑂 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥)) | 
| 206 | 190, 205 | mpd 15 | . 2
⊢ (𝜑 → ∃𝑥 ∈ (𝒫 𝑂 ∩ Fin)𝑆 ⊆ ∪ 𝑥) | 
| 207 | 148, 206 | r19.29a 3161 | 1
⊢ (𝜑 → ∃𝑧 ∈ 𝐽 (𝐴 ∈ 𝑧 ∧ ((cls‘𝐽)‘𝑧) ⊆ (𝑋 ∖ 𝑆))) |