| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ptcls.a | . . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 2 |  | ptcls.j | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑅 ∈ (TopOn‘𝑋)) | 
| 3 |  | topontop 22919 | . . . . . 6
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top) | 
| 4 | 2, 3 | syl 17 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑅 ∈ Top) | 
| 5 |  | ptcls.c | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ 𝑋) | 
| 6 |  | toponuni 22920 | . . . . . . . 8
⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑅) | 
| 7 | 2, 6 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 = ∪ 𝑅) | 
| 8 | 5, 7 | sseqtrd 4020 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ ∪ 𝑅) | 
| 9 |  | eqid 2737 | . . . . . . 7
⊢ ∪ 𝑅 =
∪ 𝑅 | 
| 10 | 9 | clscld 23055 | . . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅)
→ ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝑅)) | 
| 11 | 4, 8, 10 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝑅)) | 
| 12 | 1, 4, 11 | ptcldmpt 23622 | . . . 4
⊢ (𝜑 → X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ∈
(Clsd‘(∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅)))) | 
| 13 |  | ptcls.2 | . . . . 5
⊢ 𝐽 =
(∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅)) | 
| 14 | 13 | fveq2i 6909 | . . . 4
⊢
(Clsd‘𝐽) =
(Clsd‘(∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅))) | 
| 15 | 12, 14 | eleqtrrdi 2852 | . . 3
⊢ (𝜑 → X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝐽)) | 
| 16 | 9 | sscls 23064 | . . . . . 6
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅)
→ 𝑆 ⊆
((cls‘𝑅)‘𝑆)) | 
| 17 | 4, 8, 16 | syl2anc 584 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ⊆ ((cls‘𝑅)‘𝑆)) | 
| 18 | 17 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑆 ⊆ ((cls‘𝑅)‘𝑆)) | 
| 19 |  | ss2ixp 8950 | . . . 4
⊢
(∀𝑘 ∈
𝐴 𝑆 ⊆ ((cls‘𝑅)‘𝑆) → X𝑘 ∈ 𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) | 
| 20 | 18, 19 | syl 17 | . . 3
⊢ (𝜑 → X𝑘 ∈
𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) | 
| 21 |  | eqid 2737 | . . . 4
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 22 | 21 | clsss2 23080 | . . 3
⊢ ((X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝐽) ∧ X𝑘 ∈ 𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆) ⊆ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) | 
| 23 | 15, 20, 22 | syl2anc 584 | . 2
⊢ (𝜑 → ((cls‘𝐽)‘X𝑘 ∈
𝐴 𝑆) ⊆ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) | 
| 24 |  | vex 3484 | . . . . . 6
⊢ 𝑢 ∈ V | 
| 25 |  | eqeq1 2741 | . . . . . . . 8
⊢ (𝑥 = 𝑢 → (𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) ↔ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))) | 
| 26 | 25 | anbi2d 630 | . . . . . . 7
⊢ (𝑥 = 𝑢 → (((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ↔ ((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)))) | 
| 27 | 26 | exbidv 1921 | . . . . . 6
⊢ (𝑥 = 𝑢 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)))) | 
| 28 | 24, 27 | elab 3679 | . . . . 5
⊢ (𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))) | 
| 29 |  | nffvmpt1 6917 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) | 
| 30 | 29 | nfel2 2924 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) | 
| 31 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦(𝑔‘𝑘) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘) | 
| 32 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑘 → (𝑔‘𝑦) = (𝑔‘𝑘)) | 
| 33 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑘 → ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) = ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘)) | 
| 34 | 32, 33 | eleq12d 2835 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑘 → ((𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ↔ (𝑔‘𝑘) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘))) | 
| 35 | 30, 31, 34 | cbvralw 3306 | . . . . . . . . . . . . . 14
⊢
(∀𝑦 ∈
𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ↔ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘)) | 
| 36 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝐴) | 
| 37 |  | eqid 2737 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝐴 ↦ 𝑅) = (𝑘 ∈ 𝐴 ↦ 𝑅) | 
| 38 | 37 | fvmpt2 7027 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈ 𝐴 ∧ 𝑅 ∈ (TopOn‘𝑋)) → ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘) = 𝑅) | 
| 39 | 36, 2, 38 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘) = 𝑅) | 
| 40 | 39 | eleq2d 2827 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑔‘𝑘) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘) ↔ (𝑔‘𝑘) ∈ 𝑅)) | 
| 41 | 40 | ralbidva 3176 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑘) ↔ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅)) | 
| 42 | 35, 41 | bitrid 283 | . . . . . . . . . . . . 13
⊢ (𝜑 → (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ↔ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅)) | 
| 43 | 42 | anbi2d 630 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ↔ (𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅))) | 
| 44 | 43 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → ((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ↔ (𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅))) | 
| 45 | 44 | biimpa 476 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦))) → (𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅)) | 
| 46 |  | ptclsg.1 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∪ 𝑘 ∈ 𝐴 𝑆 ∈ AC 𝐴) | 
| 47 | 46 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∪ 𝑘 ∈ 𝐴 𝑆 ∈ AC 𝐴) | 
| 48 |  | simpll 767 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → 𝜑) | 
| 49 |  | vex 3484 | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝑓 ∈ V | 
| 50 | 49 | elixp 8944 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆))) | 
| 51 | 50 | simprbi 496 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆)) | 
| 52 | 51 | ad2antlr 727 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆)) | 
| 53 | 9 | clsndisj 23083 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅
∧ (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆)) ∧ ((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘))) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅) | 
| 54 | 53 | ex 412 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅
∧ (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆)) → (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅)) | 
| 55 | 54 | 3expia 1122 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅)
→ ((𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆) → (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅))) | 
| 56 | 4, 8, 55 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆) → (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅))) | 
| 57 | 56 | ralimdva 3167 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ ((cls‘𝑅)‘𝑆) → ∀𝑘 ∈ 𝐴 (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅))) | 
| 58 | 48, 52, 57 | sylc 65 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅)) | 
| 59 |  | simprlr 780 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) | 
| 60 |  | simprr 773 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦)) | 
| 61 | 32 | cbvixpv 8955 | . . . . . . . . . . . . . . . . . . 19
⊢ X𝑦 ∈
𝐴 (𝑔‘𝑦) = X𝑘 ∈ 𝐴 (𝑔‘𝑘) | 
| 62 | 60, 61 | eleqtrdi 2851 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → 𝑓 ∈ X𝑘 ∈ 𝐴 (𝑔‘𝑘)) | 
| 63 | 49 | elixp 8944 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 (𝑔‘𝑘) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (𝑔‘𝑘))) | 
| 64 | 63 | simprbi 496 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑓 ∈ X𝑘 ∈
𝐴 (𝑔‘𝑘) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (𝑔‘𝑘)) | 
| 65 | 62, 64 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (𝑔‘𝑘)) | 
| 66 |  | r19.26 3111 | . . . . . . . . . . . . . . . . 17
⊢
(∀𝑘 ∈
𝐴 ((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) ↔ (∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (𝑔‘𝑘))) | 
| 67 | 59, 65, 66 | sylanbrc 583 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘))) | 
| 68 |  | ralim 3086 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑘 ∈
𝐴 (((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅) → (∀𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∈ 𝑅 ∧ (𝑓‘𝑘) ∈ (𝑔‘𝑘)) → ∀𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅)) | 
| 69 | 58, 67, 68 | sylc 65 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅) | 
| 70 |  | rabn0 4389 | . . . . . . . . . . . . . . . . 17
⊢ ({𝑧 ∈ ∪ 𝑘 ∈ 𝐴 𝑆 ∣ 𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)} ≠ ∅ ↔ ∃𝑧 ∈ ∪ 𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)) | 
| 71 |  | dfin5 3959 | . . . . . . . . . . . . . . . . . . 19
⊢ (∪ 𝑘 ∈ 𝐴 𝑆 ∩ ((𝑔‘𝑘) ∩ 𝑆)) = {𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆 ∣ 𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)} | 
| 72 |  | inss2 4238 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑔‘𝑘) ∩ 𝑆) ⊆ 𝑆 | 
| 73 |  | ssiun2 5047 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ 𝐴 → 𝑆 ⊆ ∪
𝑘 ∈ 𝐴 𝑆) | 
| 74 | 72, 73 | sstrid 3995 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ 𝐴 → ((𝑔‘𝑘) ∩ 𝑆) ⊆ ∪ 𝑘 ∈ 𝐴 𝑆) | 
| 75 |  | sseqin2 4223 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔‘𝑘) ∩ 𝑆) ⊆ ∪ 𝑘 ∈ 𝐴 𝑆 ↔ (∪
𝑘 ∈ 𝐴 𝑆 ∩ ((𝑔‘𝑘) ∩ 𝑆)) = ((𝑔‘𝑘) ∩ 𝑆)) | 
| 76 | 74, 75 | sylib 218 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ 𝐴 → (∪
𝑘 ∈ 𝐴 𝑆 ∩ ((𝑔‘𝑘) ∩ 𝑆)) = ((𝑔‘𝑘) ∩ 𝑆)) | 
| 77 | 71, 76 | eqtr3id 2791 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ 𝐴 → {𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆 ∣ 𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)} = ((𝑔‘𝑘) ∩ 𝑆)) | 
| 78 | 77 | neeq1d 3000 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝐴 → ({𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆 ∣ 𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)} ≠ ∅ ↔ ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅)) | 
| 79 | 70, 78 | bitr3id 285 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ 𝐴 → (∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅)) | 
| 80 | 79 | ralbiia 3091 | . . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ ∀𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅) | 
| 81 | 69, 80 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑘 ∈ 𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆)) | 
| 82 |  | nfv 1914 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑦∃𝑧 ∈ ∪ 𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) | 
| 83 |  | nfiu1 5027 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘∪ 𝑘 ∈ 𝐴 𝑆 | 
| 84 |  | nfcv 2905 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘(𝑔‘𝑦) | 
| 85 |  | nfcsb1v 3923 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌𝑆 | 
| 86 | 84, 85 | nfin 4224 | . . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆) | 
| 87 | 86 | nfel2 2924 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘 𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆) | 
| 88 | 83, 87 | nfrexw 3313 | . . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘∃𝑧 ∈ ∪ 𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆) | 
| 89 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → (𝑔‘𝑘) = (𝑔‘𝑦)) | 
| 90 |  | csbeq1a 3913 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑦 → 𝑆 = ⦋𝑦 / 𝑘⦌𝑆) | 
| 91 | 89, 90 | ineq12d 4221 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → ((𝑔‘𝑘) ∩ 𝑆) = ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) | 
| 92 | 91 | eleq2d 2827 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑦 → (𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ 𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) | 
| 93 | 92 | rexbidv 3179 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑦 → (∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) | 
| 94 | 82, 88, 93 | cbvralw 3306 | . . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) | 
| 95 | 81, 94 | sylib 218 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) | 
| 96 |  | eleq1 2829 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (ℎ‘𝑦) → (𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆) ↔ (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) | 
| 97 | 96 | acni3 10087 | . . . . . . . . . . . . 13
⊢
((∪ 𝑘 ∈ 𝐴 𝑆 ∈ AC 𝐴 ∧ ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ ∪
𝑘 ∈ 𝐴 𝑆𝑧 ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) → ∃ℎ(ℎ:𝐴⟶∪
𝑘 ∈ 𝐴 𝑆 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) | 
| 98 | 47, 95, 97 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → ∃ℎ(ℎ:𝐴⟶∪
𝑘 ∈ 𝐴 𝑆 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) | 
| 99 |  | ffn 6736 | . . . . . . . . . . . . . 14
⊢ (ℎ:𝐴⟶∪
𝑘 ∈ 𝐴 𝑆 → ℎ Fn 𝐴) | 
| 100 |  | nfv 1914 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑦(ℎ‘𝑘) ∈ ((𝑔‘𝑘) ∩ 𝑆) | 
| 101 | 86 | nfel2 2924 | . . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆) | 
| 102 |  | fveq2 6906 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑦 → (ℎ‘𝑘) = (ℎ‘𝑦)) | 
| 103 | 102, 91 | eleq12d 2835 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑦 → ((ℎ‘𝑘) ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆))) | 
| 104 | 100, 101,
103 | cbvralw 3306 | . . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
𝐴 (ℎ‘𝑘) ∈ ((𝑔‘𝑘) ∩ 𝑆) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) | 
| 105 |  | ne0i 4341 | . . . . . . . . . . . . . . . 16
⊢ (ℎ ∈ X𝑘 ∈
𝐴 ((𝑔‘𝑘) ∩ 𝑆) → X𝑘 ∈ 𝐴 ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅) | 
| 106 |  | vex 3484 | . . . . . . . . . . . . . . . . 17
⊢ ℎ ∈ V | 
| 107 | 106 | elixp 8944 | . . . . . . . . . . . . . . . 16
⊢ (ℎ ∈ X𝑘 ∈
𝐴 ((𝑔‘𝑘) ∩ 𝑆) ↔ (ℎ Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (ℎ‘𝑘) ∈ ((𝑔‘𝑘) ∩ 𝑆))) | 
| 108 |  | ixpin 8963 | . . . . . . . . . . . . . . . . . 18
⊢ X𝑘 ∈
𝐴 ((𝑔‘𝑘) ∩ 𝑆) = (X𝑘 ∈ 𝐴 (𝑔‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) | 
| 109 | 61 | ineq1i 4216 | . . . . . . . . . . . . . . . . . 18
⊢ (X𝑦 ∈
𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) = (X𝑘 ∈ 𝐴 (𝑔‘𝑘) ∩ X𝑘 ∈ 𝐴 𝑆) | 
| 110 | 108, 109 | eqtr4i 2768 | . . . . . . . . . . . . . . . . 17
⊢ X𝑘 ∈
𝐴 ((𝑔‘𝑘) ∩ 𝑆) = (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) | 
| 111 | 110 | neeq1i 3005 | . . . . . . . . . . . . . . . 16
⊢ (X𝑘 ∈
𝐴 ((𝑔‘𝑘) ∩ 𝑆) ≠ ∅ ↔ (X𝑦 ∈
𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) | 
| 112 | 105, 107,
111 | 3imtr3i 291 | . . . . . . . . . . . . . . 15
⊢ ((ℎ Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (ℎ‘𝑘) ∈ ((𝑔‘𝑘) ∩ 𝑆)) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) | 
| 113 | 104, 112 | sylan2br 595 | . . . . . . . . . . . . . 14
⊢ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) | 
| 114 | 99, 113 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((ℎ:𝐴⟶∪
𝑘 ∈ 𝐴 𝑆 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) | 
| 115 | 114 | exlimiv 1930 | . . . . . . . . . . . 12
⊢
(∃ℎ(ℎ:𝐴⟶∪
𝑘 ∈ 𝐴 𝑆 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ ((𝑔‘𝑦) ∩ ⦋𝑦 / 𝑘⦌𝑆)) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) | 
| 116 | 98, 115 | syl 17 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) | 
| 117 | 116 | expr 456 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑔‘𝑘) ∈ 𝑅)) → (𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅)) | 
| 118 | 45, 117 | syldan 591 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦))) → (𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅)) | 
| 119 | 118 | 3adantr3 1172 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦))) → (𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅)) | 
| 120 |  | eleq2 2830 | . . . . . . . . 9
⊢ (𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (𝑓 ∈ 𝑢 ↔ 𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦))) | 
| 121 |  | ineq1 4213 | . . . . . . . . . 10
⊢ (𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) = (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆)) | 
| 122 | 121 | neeq1d 3000 | . . . . . . . . 9
⊢ (𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅ ↔ (X𝑦 ∈
𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅)) | 
| 123 | 120, 122 | imbi12d 344 | . . . . . . . 8
⊢ (𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → ((𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅) ↔ (𝑓 ∈ X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (X𝑦 ∈ 𝐴 (𝑔‘𝑦) ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) | 
| 124 | 119, 123 | syl5ibrcom 247 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦))) → (𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦) → (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) | 
| 125 | 124 | expimpd 453 | . . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → (((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) | 
| 126 | 125 | exlimdv 1933 | . . . . 5
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑢 = X𝑦 ∈ 𝐴 (𝑔‘𝑦)) → (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) | 
| 127 | 28, 126 | biimtrid 242 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → (𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} → (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) | 
| 128 | 127 | ralrimiv 3145 | . . 3
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → ∀𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅)) | 
| 129 | 4 | fmpttd 7135 | . . . . . . . 8
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑅):𝐴⟶Top) | 
| 130 | 129 | ffnd 6737 | . . . . . . 7
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑅) Fn 𝐴) | 
| 131 |  | eqid 2737 | . . . . . . . 8
⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} | 
| 132 | 131 | ptval 23578 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ 𝑅) Fn 𝐴) → (∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅)) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) | 
| 133 | 1, 130, 132 | syl2anc 584 | . . . . . 6
⊢ (𝜑 →
(∏t‘(𝑘 ∈ 𝐴 ↦ 𝑅)) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) | 
| 134 | 13, 133 | eqtrid 2789 | . . . . 5
⊢ (𝜑 → 𝐽 = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) | 
| 135 | 134 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → 𝐽 = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) | 
| 136 | 2 | ralrimiva 3146 | . . . . . . 7
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑅 ∈ (TopOn‘𝑋)) | 
| 137 | 13 | pttopon 23604 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑘 ∈ 𝐴 𝑅 ∈ (TopOn‘𝑋)) → 𝐽 ∈ (TopOn‘X𝑘 ∈
𝐴 𝑋)) | 
| 138 | 1, 136, 137 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → 𝐽 ∈ (TopOn‘X𝑘 ∈
𝐴 𝑋)) | 
| 139 |  | toponuni 22920 | . . . . . 6
⊢ (𝐽 ∈ (TopOn‘X𝑘 ∈
𝐴 𝑋) → X𝑘 ∈ 𝐴 𝑋 = ∪ 𝐽) | 
| 140 | 138, 139 | syl 17 | . . . . 5
⊢ (𝜑 → X𝑘 ∈
𝐴 𝑋 = ∪ 𝐽) | 
| 141 | 140 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → X𝑘 ∈ 𝐴 𝑋 = ∪ 𝐽) | 
| 142 | 131 | ptbas 23587 | . . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑘 ∈ 𝐴 ↦ 𝑅):𝐴⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ∈ TopBases) | 
| 143 | 1, 129, 142 | syl2anc 584 | . . . . 5
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ∈ TopBases) | 
| 144 | 143 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} ∈ TopBases) | 
| 145 | 5 | ralrimiva 3146 | . . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝑆 ⊆ 𝑋) | 
| 146 |  | ss2ixp 8950 | . . . . . 6
⊢
(∀𝑘 ∈
𝐴 𝑆 ⊆ 𝑋 → X𝑘 ∈ 𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 𝑋) | 
| 147 | 145, 146 | syl 17 | . . . . 5
⊢ (𝜑 → X𝑘 ∈
𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 𝑋) | 
| 148 | 147 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → X𝑘 ∈ 𝐴 𝑆 ⊆ X𝑘 ∈ 𝐴 𝑋) | 
| 149 | 9 | clsss3 23067 | . . . . . . . . 9
⊢ ((𝑅 ∈ Top ∧ 𝑆 ⊆ ∪ 𝑅)
→ ((cls‘𝑅)‘𝑆) ⊆ ∪ 𝑅) | 
| 150 | 4, 8, 149 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((cls‘𝑅)‘𝑆) ⊆ ∪ 𝑅) | 
| 151 | 150, 7 | sseqtrrd 4021 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((cls‘𝑅)‘𝑆) ⊆ 𝑋) | 
| 152 | 151 | ralrimiva 3146 | . . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆) ⊆ 𝑋) | 
| 153 |  | ss2ixp 8950 | . . . . . 6
⊢
(∀𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ⊆ 𝑋 → X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆) ⊆ X𝑘 ∈ 𝐴 𝑋) | 
| 154 | 152, 153 | syl 17 | . . . . 5
⊢ (𝜑 → X𝑘 ∈
𝐴 ((cls‘𝑅)‘𝑆) ⊆ X𝑘 ∈ 𝐴 𝑋) | 
| 155 | 154 | sselda 3983 | . . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → 𝑓 ∈ X𝑘 ∈ 𝐴 𝑋) | 
| 156 | 135, 141,
144, 148, 155 | elcls3 23091 | . . 3
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → (𝑓 ∈ ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆) ↔ ∀𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ ((𝑘 ∈ 𝐴 ↦ 𝑅)‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} (𝑓 ∈ 𝑢 → (𝑢 ∩ X𝑘 ∈ 𝐴 𝑆) ≠ ∅))) | 
| 157 | 128, 156 | mpbird 257 | . 2
⊢ ((𝜑 ∧ 𝑓 ∈ X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) → 𝑓 ∈ ((cls‘𝐽)‘X𝑘 ∈ 𝐴 𝑆)) | 
| 158 | 23, 157 | eqelssd 4005 | 1
⊢ (𝜑 → ((cls‘𝐽)‘X𝑘 ∈
𝐴 𝑆) = X𝑘 ∈ 𝐴 ((cls‘𝑅)‘𝑆)) |