| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eleq2w 2825 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑃 ∈ 𝑦 ↔ 𝑃 ∈ 𝑧)) | 
| 2 |  | eqeq1 2741 | . . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑦 = (𝑆 ∪ {𝑃}) ↔ 𝑧 = (𝑆 ∪ {𝑃}))) | 
| 3 | 1, 2 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝑃 ∈ 𝑦 → 𝑦 = (𝑆 ∪ {𝑃})) ↔ (𝑃 ∈ 𝑧 → 𝑧 = (𝑆 ∪ {𝑃})))) | 
| 4 |  | dfac14lem.r | . . . . . . . . . 10
⊢ 𝑅 = {𝑦 ∈ 𝒫 (𝑆 ∪ {𝑃}) ∣ (𝑃 ∈ 𝑦 → 𝑦 = (𝑆 ∪ {𝑃}))} | 
| 5 | 3, 4 | elrab2 3695 | . . . . . . . . 9
⊢ (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ 𝒫 (𝑆 ∪ {𝑃}) ∧ (𝑃 ∈ 𝑧 → 𝑧 = (𝑆 ∪ {𝑃})))) | 
| 6 |  | dfac14lem.0 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅) | 
| 7 | 6 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝒫 (𝑆 ∪ {𝑃})) → 𝑆 ≠ ∅) | 
| 8 |  | ineq1 4213 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑆 ∪ {𝑃}) → (𝑧 ∩ 𝑆) = ((𝑆 ∪ {𝑃}) ∩ 𝑆)) | 
| 9 |  | ssun1 4178 | . . . . . . . . . . . . . . 15
⊢ 𝑆 ⊆ (𝑆 ∪ {𝑃}) | 
| 10 |  | sseqin2 4223 | . . . . . . . . . . . . . . 15
⊢ (𝑆 ⊆ (𝑆 ∪ {𝑃}) ↔ ((𝑆 ∪ {𝑃}) ∩ 𝑆) = 𝑆) | 
| 11 | 9, 10 | mpbi 230 | . . . . . . . . . . . . . 14
⊢ ((𝑆 ∪ {𝑃}) ∩ 𝑆) = 𝑆 | 
| 12 | 8, 11 | eqtrdi 2793 | . . . . . . . . . . . . 13
⊢ (𝑧 = (𝑆 ∪ {𝑃}) → (𝑧 ∩ 𝑆) = 𝑆) | 
| 13 | 12 | neeq1d 3000 | . . . . . . . . . . . 12
⊢ (𝑧 = (𝑆 ∪ {𝑃}) → ((𝑧 ∩ 𝑆) ≠ ∅ ↔ 𝑆 ≠ ∅)) | 
| 14 | 7, 13 | syl5ibrcom 247 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝒫 (𝑆 ∪ {𝑃})) → (𝑧 = (𝑆 ∪ {𝑃}) → (𝑧 ∩ 𝑆) ≠ ∅)) | 
| 15 | 14 | imim2d 57 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑧 ∈ 𝒫 (𝑆 ∪ {𝑃})) → ((𝑃 ∈ 𝑧 → 𝑧 = (𝑆 ∪ {𝑃})) → (𝑃 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))) | 
| 16 | 15 | expimpd 453 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑧 ∈ 𝒫 (𝑆 ∪ {𝑃}) ∧ (𝑃 ∈ 𝑧 → 𝑧 = (𝑆 ∪ {𝑃}))) → (𝑃 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))) | 
| 17 | 5, 16 | biimtrid 242 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑧 ∈ 𝑅 → (𝑃 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))) | 
| 18 | 17 | ralrimiv 3145 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∀𝑧 ∈ 𝑅 (𝑃 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅)) | 
| 19 |  | dfac14lem.s | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ∈ 𝑊) | 
| 20 |  | snex 5436 | . . . . . . . . . . . 12
⊢ {𝑃} ∈ V | 
| 21 |  | unexg 7763 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑊 ∧ {𝑃} ∈ V) → (𝑆 ∪ {𝑃}) ∈ V) | 
| 22 | 19, 20, 21 | sylancl 586 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆 ∪ {𝑃}) ∈ V) | 
| 23 |  | ssun2 4179 | . . . . . . . . . . . 12
⊢ {𝑃} ⊆ (𝑆 ∪ {𝑃}) | 
| 24 |  | dfac14lem.p | . . . . . . . . . . . . . 14
⊢ 𝑃 = 𝒫 ∪ 𝑆 | 
| 25 |  | uniexg 7760 | . . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ 𝑊 → ∪ 𝑆 ∈ V) | 
| 26 |  | pwexg 5378 | . . . . . . . . . . . . . . 15
⊢ (∪ 𝑆
∈ V → 𝒫 ∪ 𝑆 ∈ V) | 
| 27 | 19, 25, 26 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝒫 ∪ 𝑆
∈ V) | 
| 28 | 24, 27 | eqeltrid 2845 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑃 ∈ V) | 
| 29 |  | snidg 4660 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ V → 𝑃 ∈ {𝑃}) | 
| 30 | 28, 29 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑃 ∈ {𝑃}) | 
| 31 | 23, 30 | sselid 3981 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑃 ∈ (𝑆 ∪ {𝑃})) | 
| 32 |  | epttop 23016 | . . . . . . . . . . 11
⊢ (((𝑆 ∪ {𝑃}) ∈ V ∧ 𝑃 ∈ (𝑆 ∪ {𝑃})) → {𝑦 ∈ 𝒫 (𝑆 ∪ {𝑃}) ∣ (𝑃 ∈ 𝑦 → 𝑦 = (𝑆 ∪ {𝑃}))} ∈ (TopOn‘(𝑆 ∪ {𝑃}))) | 
| 33 | 22, 31, 32 | syl2anc 584 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → {𝑦 ∈ 𝒫 (𝑆 ∪ {𝑃}) ∣ (𝑃 ∈ 𝑦 → 𝑦 = (𝑆 ∪ {𝑃}))} ∈ (TopOn‘(𝑆 ∪ {𝑃}))) | 
| 34 | 4, 33 | eqeltrid 2845 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ (TopOn‘(𝑆 ∪ {𝑃}))) | 
| 35 |  | topontop 22919 | . . . . . . . . 9
⊢ (𝑅 ∈ (TopOn‘(𝑆 ∪ {𝑃})) → 𝑅 ∈ Top) | 
| 36 | 34, 35 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Top) | 
| 37 |  | toponuni 22920 | . . . . . . . . . 10
⊢ (𝑅 ∈ (TopOn‘(𝑆 ∪ {𝑃})) → (𝑆 ∪ {𝑃}) = ∪ 𝑅) | 
| 38 | 34, 37 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑆 ∪ {𝑃}) = ∪ 𝑅) | 
| 39 | 9, 38 | sseqtrid 4026 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ⊆ ∪ 𝑅) | 
| 40 | 31, 38 | eleqtrd 2843 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑃 ∈ ∪ 𝑅) | 
| 41 |  | eqid 2737 | . . . . . . . . 9
⊢ ∪ 𝑅 =
∪ 𝑅 | 
| 42 | 41 | elcls 23081 | . . . . . . . 8
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅
∧ 𝑃 ∈ ∪ 𝑅)
→ (𝑃 ∈
((cls‘𝑅)‘𝑆) ↔ ∀𝑧 ∈ 𝑅 (𝑃 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))) | 
| 43 | 36, 39, 40, 42 | syl3anc 1373 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑃 ∈ ((cls‘𝑅)‘𝑆) ↔ ∀𝑧 ∈ 𝑅 (𝑃 ∈ 𝑧 → (𝑧 ∩ 𝑆) ≠ ∅))) | 
| 44 | 18, 43 | mpbird 257 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑃 ∈ ((cls‘𝑅)‘𝑆)) | 
| 45 | 44 | ralrimiva 3146 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑃 ∈ ((cls‘𝑅)‘𝑆)) | 
| 46 |  | dfac14lem.i | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 47 |  | mptelixpg 8975 | . . . . . 6
⊢ (𝐼 ∈ 𝑉 → ((𝑥 ∈ 𝐼 ↦ 𝑃) ∈ X𝑥 ∈ 𝐼 ((cls‘𝑅)‘𝑆) ↔ ∀𝑥 ∈ 𝐼 𝑃 ∈ ((cls‘𝑅)‘𝑆))) | 
| 48 | 46, 47 | syl 17 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑃) ∈ X𝑥 ∈ 𝐼 ((cls‘𝑅)‘𝑆) ↔ ∀𝑥 ∈ 𝐼 𝑃 ∈ ((cls‘𝑅)‘𝑆))) | 
| 49 | 45, 48 | mpbird 257 | . . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑃) ∈ X𝑥 ∈ 𝐼 ((cls‘𝑅)‘𝑆)) | 
| 50 | 49 | ne0d 4342 | . . 3
⊢ (𝜑 → X𝑥 ∈
𝐼 ((cls‘𝑅)‘𝑆) ≠ ∅) | 
| 51 |  | dfac14lem.c | . . 3
⊢ (𝜑 → ((cls‘𝐽)‘X𝑥 ∈
𝐼 𝑆) = X𝑥 ∈ 𝐼 ((cls‘𝑅)‘𝑆)) | 
| 52 | 34 | ralrimiva 3146 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝑅 ∈ (TopOn‘(𝑆 ∪ {𝑃}))) | 
| 53 |  | dfac14lem.j | . . . . . 6
⊢ 𝐽 =
(∏t‘(𝑥 ∈ 𝐼 ↦ 𝑅)) | 
| 54 | 53 | pttopon 23604 | . . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐼 𝑅 ∈ (TopOn‘(𝑆 ∪ {𝑃}))) → 𝐽 ∈ (TopOn‘X𝑥 ∈
𝐼 (𝑆 ∪ {𝑃}))) | 
| 55 | 46, 52, 54 | syl2anc 584 | . . . 4
⊢ (𝜑 → 𝐽 ∈ (TopOn‘X𝑥 ∈
𝐼 (𝑆 ∪ {𝑃}))) | 
| 56 |  | topontop 22919 | . . . 4
⊢ (𝐽 ∈ (TopOn‘X𝑥 ∈
𝐼 (𝑆 ∪ {𝑃})) → 𝐽 ∈ Top) | 
| 57 |  | cls0 23088 | . . . 4
⊢ (𝐽 ∈ Top →
((cls‘𝐽)‘∅) = ∅) | 
| 58 | 55, 56, 57 | 3syl 18 | . . 3
⊢ (𝜑 → ((cls‘𝐽)‘∅) =
∅) | 
| 59 | 50, 51, 58 | 3netr4d 3018 | . 2
⊢ (𝜑 → ((cls‘𝐽)‘X𝑥 ∈
𝐼 𝑆) ≠ ((cls‘𝐽)‘∅)) | 
| 60 |  | fveq2 6906 | . . 3
⊢ (X𝑥 ∈
𝐼 𝑆 = ∅ → ((cls‘𝐽)‘X𝑥 ∈
𝐼 𝑆) = ((cls‘𝐽)‘∅)) | 
| 61 | 60 | necon3i 2973 | . 2
⊢
(((cls‘𝐽)‘X𝑥 ∈ 𝐼 𝑆) ≠ ((cls‘𝐽)‘∅) → X𝑥 ∈
𝐼 𝑆 ≠ ∅) | 
| 62 | 59, 61 | syl 17 | 1
⊢ (𝜑 → X𝑥 ∈
𝐼 𝑆 ≠ ∅) |