MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ptclsg Structured version   Visualization version   GIF version

Theorem ptclsg 23101
Description: The closure of a box in the product topology is the box formed from the closures of the factors. The proof uses the axiom of choice; the last hypothesis is the choice assumption. (Contributed by Mario Carneiro, 3-Sep-2015.)
Hypotheses
Ref Expression
ptcls.2 𝐽 = (∏t‘(𝑘𝐴𝑅))
ptcls.a (𝜑𝐴𝑉)
ptcls.j ((𝜑𝑘𝐴) → 𝑅 ∈ (TopOn‘𝑋))
ptcls.c ((𝜑𝑘𝐴) → 𝑆𝑋)
ptclsg.1 (𝜑 𝑘𝐴 𝑆AC 𝐴)
Assertion
Ref Expression
ptclsg (𝜑 → ((cls‘𝐽)‘X𝑘𝐴 𝑆) = X𝑘𝐴 ((cls‘𝑅)‘𝑆))
Distinct variable groups:   𝜑,𝑘   𝐴,𝑘
Allowed substitution hints:   𝑅(𝑘)   𝑆(𝑘)   𝐽(𝑘)   𝑉(𝑘)   𝑋(𝑘)

Proof of Theorem ptclsg
Dummy variables 𝑓 𝑔 𝑢 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptcls.a . . . . 5 (𝜑𝐴𝑉)
2 ptcls.j . . . . . 6 ((𝜑𝑘𝐴) → 𝑅 ∈ (TopOn‘𝑋))
3 topontop 22397 . . . . . 6 (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top)
42, 3syl 17 . . . . 5 ((𝜑𝑘𝐴) → 𝑅 ∈ Top)
5 ptcls.c . . . . . . 7 ((𝜑𝑘𝐴) → 𝑆𝑋)
6 toponuni 22398 . . . . . . . 8 (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = 𝑅)
72, 6syl 17 . . . . . . 7 ((𝜑𝑘𝐴) → 𝑋 = 𝑅)
85, 7sseqtrd 4021 . . . . . 6 ((𝜑𝑘𝐴) → 𝑆 𝑅)
9 eqid 2733 . . . . . . 7 𝑅 = 𝑅
109clscld 22533 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 𝑅) → ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝑅))
114, 8, 10syl2anc 585 . . . . 5 ((𝜑𝑘𝐴) → ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝑅))
121, 4, 11ptcldmpt 23100 . . . 4 (𝜑X𝑘𝐴 ((cls‘𝑅)‘𝑆) ∈ (Clsd‘(∏t‘(𝑘𝐴𝑅))))
13 ptcls.2 . . . . 5 𝐽 = (∏t‘(𝑘𝐴𝑅))
1413fveq2i 6891 . . . 4 (Clsd‘𝐽) = (Clsd‘(∏t‘(𝑘𝐴𝑅)))
1512, 14eleqtrrdi 2845 . . 3 (𝜑X𝑘𝐴 ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝐽))
169sscls 22542 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 𝑅) → 𝑆 ⊆ ((cls‘𝑅)‘𝑆))
174, 8, 16syl2anc 585 . . . . 5 ((𝜑𝑘𝐴) → 𝑆 ⊆ ((cls‘𝑅)‘𝑆))
1817ralrimiva 3147 . . . 4 (𝜑 → ∀𝑘𝐴 𝑆 ⊆ ((cls‘𝑅)‘𝑆))
19 ss2ixp 8900 . . . 4 (∀𝑘𝐴 𝑆 ⊆ ((cls‘𝑅)‘𝑆) → X𝑘𝐴 𝑆X𝑘𝐴 ((cls‘𝑅)‘𝑆))
2018, 19syl 17 . . 3 (𝜑X𝑘𝐴 𝑆X𝑘𝐴 ((cls‘𝑅)‘𝑆))
21 eqid 2733 . . . 4 𝐽 = 𝐽
2221clsss2 22558 . . 3 ((X𝑘𝐴 ((cls‘𝑅)‘𝑆) ∈ (Clsd‘𝐽) ∧ X𝑘𝐴 𝑆X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → ((cls‘𝐽)‘X𝑘𝐴 𝑆) ⊆ X𝑘𝐴 ((cls‘𝑅)‘𝑆))
2315, 20, 22syl2anc 585 . 2 (𝜑 → ((cls‘𝐽)‘X𝑘𝐴 𝑆) ⊆ X𝑘𝐴 ((cls‘𝑅)‘𝑆))
24 vex 3479 . . . . . 6 𝑢 ∈ V
25 eqeq1 2737 . . . . . . . 8 (𝑥 = 𝑢 → (𝑥 = X𝑦𝐴 (𝑔𝑦) ↔ 𝑢 = X𝑦𝐴 (𝑔𝑦)))
2625anbi2d 630 . . . . . . 7 (𝑥 = 𝑢 → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦)) ↔ ((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑢 = X𝑦𝐴 (𝑔𝑦))))
2726exbidv 1925 . . . . . 6 (𝑥 = 𝑢 → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦)) ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑢 = X𝑦𝐴 (𝑔𝑦))))
2824, 27elab 3667 . . . . 5 (𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} ↔ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑢 = X𝑦𝐴 (𝑔𝑦)))
29 nffvmpt1 6899 . . . . . . . . . . . . . . . 16 𝑘((𝑘𝐴𝑅)‘𝑦)
3029nfel2 2922 . . . . . . . . . . . . . . 15 𝑘(𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦)
31 nfv 1918 . . . . . . . . . . . . . . 15 𝑦(𝑔𝑘) ∈ ((𝑘𝐴𝑅)‘𝑘)
32 fveq2 6888 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑘 → (𝑔𝑦) = (𝑔𝑘))
33 fveq2 6888 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑘 → ((𝑘𝐴𝑅)‘𝑦) = ((𝑘𝐴𝑅)‘𝑘))
3432, 33eleq12d 2828 . . . . . . . . . . . . . . 15 (𝑦 = 𝑘 → ((𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ↔ (𝑔𝑘) ∈ ((𝑘𝐴𝑅)‘𝑘)))
3530, 31, 34cbvralw 3304 . . . . . . . . . . . . . 14 (∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ↔ ∀𝑘𝐴 (𝑔𝑘) ∈ ((𝑘𝐴𝑅)‘𝑘))
36 simpr 486 . . . . . . . . . . . . . . . . 17 ((𝜑𝑘𝐴) → 𝑘𝐴)
37 eqid 2733 . . . . . . . . . . . . . . . . . 18 (𝑘𝐴𝑅) = (𝑘𝐴𝑅)
3837fvmpt2 7005 . . . . . . . . . . . . . . . . 17 ((𝑘𝐴𝑅 ∈ (TopOn‘𝑋)) → ((𝑘𝐴𝑅)‘𝑘) = 𝑅)
3936, 2, 38syl2anc 585 . . . . . . . . . . . . . . . 16 ((𝜑𝑘𝐴) → ((𝑘𝐴𝑅)‘𝑘) = 𝑅)
4039eleq2d 2820 . . . . . . . . . . . . . . 15 ((𝜑𝑘𝐴) → ((𝑔𝑘) ∈ ((𝑘𝐴𝑅)‘𝑘) ↔ (𝑔𝑘) ∈ 𝑅))
4140ralbidva 3176 . . . . . . . . . . . . . 14 (𝜑 → (∀𝑘𝐴 (𝑔𝑘) ∈ ((𝑘𝐴𝑅)‘𝑘) ↔ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅))
4235, 41bitrid 283 . . . . . . . . . . . . 13 (𝜑 → (∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ↔ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅))
4342anbi2d 630 . . . . . . . . . . . 12 (𝜑 → ((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦)) ↔ (𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅)))
4443adantr 482 . . . . . . . . . . 11 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → ((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦)) ↔ (𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅)))
4544biimpa 478 . . . . . . . . . 10 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦))) → (𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅))
46 ptclsg.1 . . . . . . . . . . . . . 14 (𝜑 𝑘𝐴 𝑆AC 𝐴)
4746ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → 𝑘𝐴 𝑆AC 𝐴)
48 simpll 766 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → 𝜑)
49 vex 3479 . . . . . . . . . . . . . . . . . . . 20 𝑓 ∈ V
5049elixp 8894 . . . . . . . . . . . . . . . . . . 19 (𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ((cls‘𝑅)‘𝑆)))
5150simprbi 498 . . . . . . . . . . . . . . . . . 18 (𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆) → ∀𝑘𝐴 (𝑓𝑘) ∈ ((cls‘𝑅)‘𝑆))
5251ad2antlr 726 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → ∀𝑘𝐴 (𝑓𝑘) ∈ ((cls‘𝑅)‘𝑆))
539clsndisj 22561 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ Top ∧ 𝑆 𝑅 ∧ (𝑓𝑘) ∈ ((cls‘𝑅)‘𝑆)) ∧ ((𝑔𝑘) ∈ 𝑅 ∧ (𝑓𝑘) ∈ (𝑔𝑘))) → ((𝑔𝑘) ∩ 𝑆) ≠ ∅)
5453ex 414 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ Top ∧ 𝑆 𝑅 ∧ (𝑓𝑘) ∈ ((cls‘𝑅)‘𝑆)) → (((𝑔𝑘) ∈ 𝑅 ∧ (𝑓𝑘) ∈ (𝑔𝑘)) → ((𝑔𝑘) ∩ 𝑆) ≠ ∅))
55543expia 1122 . . . . . . . . . . . . . . . . . . 19 ((𝑅 ∈ Top ∧ 𝑆 𝑅) → ((𝑓𝑘) ∈ ((cls‘𝑅)‘𝑆) → (((𝑔𝑘) ∈ 𝑅 ∧ (𝑓𝑘) ∈ (𝑔𝑘)) → ((𝑔𝑘) ∩ 𝑆) ≠ ∅)))
564, 8, 55syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘𝐴) → ((𝑓𝑘) ∈ ((cls‘𝑅)‘𝑆) → (((𝑔𝑘) ∈ 𝑅 ∧ (𝑓𝑘) ∈ (𝑔𝑘)) → ((𝑔𝑘) ∩ 𝑆) ≠ ∅)))
5756ralimdva 3168 . . . . . . . . . . . . . . . . 17 (𝜑 → (∀𝑘𝐴 (𝑓𝑘) ∈ ((cls‘𝑅)‘𝑆) → ∀𝑘𝐴 (((𝑔𝑘) ∈ 𝑅 ∧ (𝑓𝑘) ∈ (𝑔𝑘)) → ((𝑔𝑘) ∩ 𝑆) ≠ ∅)))
5848, 52, 57sylc 65 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → ∀𝑘𝐴 (((𝑔𝑘) ∈ 𝑅 ∧ (𝑓𝑘) ∈ (𝑔𝑘)) → ((𝑔𝑘) ∩ 𝑆) ≠ ∅))
59 simprlr 779 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅)
60 simprr 772 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → 𝑓X𝑦𝐴 (𝑔𝑦))
6132cbvixpv 8905 . . . . . . . . . . . . . . . . . . 19 X𝑦𝐴 (𝑔𝑦) = X𝑘𝐴 (𝑔𝑘)
6260, 61eleqtrdi 2844 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → 𝑓X𝑘𝐴 (𝑔𝑘))
6349elixp 8894 . . . . . . . . . . . . . . . . . . 19 (𝑓X𝑘𝐴 (𝑔𝑘) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ (𝑔𝑘)))
6463simprbi 498 . . . . . . . . . . . . . . . . . 18 (𝑓X𝑘𝐴 (𝑔𝑘) → ∀𝑘𝐴 (𝑓𝑘) ∈ (𝑔𝑘))
6562, 64syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → ∀𝑘𝐴 (𝑓𝑘) ∈ (𝑔𝑘))
66 r19.26 3112 . . . . . . . . . . . . . . . . 17 (∀𝑘𝐴 ((𝑔𝑘) ∈ 𝑅 ∧ (𝑓𝑘) ∈ (𝑔𝑘)) ↔ (∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ (𝑔𝑘)))
6759, 65, 66sylanbrc 584 . . . . . . . . . . . . . . . 16 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → ∀𝑘𝐴 ((𝑔𝑘) ∈ 𝑅 ∧ (𝑓𝑘) ∈ (𝑔𝑘)))
68 ralim 3087 . . . . . . . . . . . . . . . 16 (∀𝑘𝐴 (((𝑔𝑘) ∈ 𝑅 ∧ (𝑓𝑘) ∈ (𝑔𝑘)) → ((𝑔𝑘) ∩ 𝑆) ≠ ∅) → (∀𝑘𝐴 ((𝑔𝑘) ∈ 𝑅 ∧ (𝑓𝑘) ∈ (𝑔𝑘)) → ∀𝑘𝐴 ((𝑔𝑘) ∩ 𝑆) ≠ ∅))
6958, 67, 68sylc 65 . . . . . . . . . . . . . . 15 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → ∀𝑘𝐴 ((𝑔𝑘) ∩ 𝑆) ≠ ∅)
70 rabn0 4384 . . . . . . . . . . . . . . . . 17 ({𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆)} ≠ ∅ ↔ ∃𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆))
71 dfin5 3955 . . . . . . . . . . . . . . . . . . 19 ( 𝑘𝐴 𝑆 ∩ ((𝑔𝑘) ∩ 𝑆)) = {𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆)}
72 inss2 4228 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔𝑘) ∩ 𝑆) ⊆ 𝑆
73 ssiun2 5049 . . . . . . . . . . . . . . . . . . . . 21 (𝑘𝐴𝑆 𝑘𝐴 𝑆)
7472, 73sstrid 3992 . . . . . . . . . . . . . . . . . . . 20 (𝑘𝐴 → ((𝑔𝑘) ∩ 𝑆) ⊆ 𝑘𝐴 𝑆)
75 sseqin2 4214 . . . . . . . . . . . . . . . . . . . 20 (((𝑔𝑘) ∩ 𝑆) ⊆ 𝑘𝐴 𝑆 ↔ ( 𝑘𝐴 𝑆 ∩ ((𝑔𝑘) ∩ 𝑆)) = ((𝑔𝑘) ∩ 𝑆))
7674, 75sylib 217 . . . . . . . . . . . . . . . . . . 19 (𝑘𝐴 → ( 𝑘𝐴 𝑆 ∩ ((𝑔𝑘) ∩ 𝑆)) = ((𝑔𝑘) ∩ 𝑆))
7771, 76eqtr3id 2787 . . . . . . . . . . . . . . . . . 18 (𝑘𝐴 → {𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆)} = ((𝑔𝑘) ∩ 𝑆))
7877neeq1d 3001 . . . . . . . . . . . . . . . . 17 (𝑘𝐴 → ({𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆)} ≠ ∅ ↔ ((𝑔𝑘) ∩ 𝑆) ≠ ∅))
7970, 78bitr3id 285 . . . . . . . . . . . . . . . 16 (𝑘𝐴 → (∃𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆) ↔ ((𝑔𝑘) ∩ 𝑆) ≠ ∅))
8079ralbiia 3092 . . . . . . . . . . . . . . 15 (∀𝑘𝐴𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆) ↔ ∀𝑘𝐴 ((𝑔𝑘) ∩ 𝑆) ≠ ∅)
8169, 80sylibr 233 . . . . . . . . . . . . . 14 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → ∀𝑘𝐴𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆))
82 nfv 1918 . . . . . . . . . . . . . . 15 𝑦𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆)
83 nfiu1 5030 . . . . . . . . . . . . . . . 16 𝑘 𝑘𝐴 𝑆
84 nfcv 2904 . . . . . . . . . . . . . . . . . 18 𝑘(𝑔𝑦)
85 nfcsb1v 3917 . . . . . . . . . . . . . . . . . 18 𝑘𝑦 / 𝑘𝑆
8684, 85nfin 4215 . . . . . . . . . . . . . . . . 17 𝑘((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)
8786nfel2 2922 . . . . . . . . . . . . . . . 16 𝑘 𝑧 ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)
8883, 87nfrexw 3311 . . . . . . . . . . . . . . 15 𝑘𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)
89 fveq2 6888 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦 → (𝑔𝑘) = (𝑔𝑦))
90 csbeq1a 3906 . . . . . . . . . . . . . . . . . 18 (𝑘 = 𝑦𝑆 = 𝑦 / 𝑘𝑆)
9189, 90ineq12d 4212 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → ((𝑔𝑘) ∩ 𝑆) = ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆))
9291eleq2d 2820 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → (𝑧 ∈ ((𝑔𝑘) ∩ 𝑆) ↔ 𝑧 ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)))
9392rexbidv 3179 . . . . . . . . . . . . . . 15 (𝑘 = 𝑦 → (∃𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆) ↔ ∃𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)))
9482, 88, 93cbvralw 3304 . . . . . . . . . . . . . 14 (∀𝑘𝐴𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑘) ∩ 𝑆) ↔ ∀𝑦𝐴𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆))
9581, 94sylib 217 . . . . . . . . . . . . 13 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → ∀𝑦𝐴𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆))
96 eleq1 2822 . . . . . . . . . . . . . 14 (𝑧 = (𝑦) → (𝑧 ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆) ↔ (𝑦) ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)))
9796acni3 10038 . . . . . . . . . . . . 13 (( 𝑘𝐴 𝑆AC 𝐴 ∧ ∀𝑦𝐴𝑧 𝑘𝐴 𝑆𝑧 ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)) → ∃(:𝐴 𝑘𝐴 𝑆 ∧ ∀𝑦𝐴 (𝑦) ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)))
9847, 95, 97syl2anc 585 . . . . . . . . . . . 12 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → ∃(:𝐴 𝑘𝐴 𝑆 ∧ ∀𝑦𝐴 (𝑦) ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)))
99 ffn 6714 . . . . . . . . . . . . . 14 (:𝐴 𝑘𝐴 𝑆 Fn 𝐴)
100 nfv 1918 . . . . . . . . . . . . . . . 16 𝑦(𝑘) ∈ ((𝑔𝑘) ∩ 𝑆)
10186nfel2 2922 . . . . . . . . . . . . . . . 16 𝑘(𝑦) ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)
102 fveq2 6888 . . . . . . . . . . . . . . . . 17 (𝑘 = 𝑦 → (𝑘) = (𝑦))
103102, 91eleq12d 2828 . . . . . . . . . . . . . . . 16 (𝑘 = 𝑦 → ((𝑘) ∈ ((𝑔𝑘) ∩ 𝑆) ↔ (𝑦) ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)))
104100, 101, 103cbvralw 3304 . . . . . . . . . . . . . . 15 (∀𝑘𝐴 (𝑘) ∈ ((𝑔𝑘) ∩ 𝑆) ↔ ∀𝑦𝐴 (𝑦) ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆))
105 ne0i 4333 . . . . . . . . . . . . . . . 16 (X𝑘𝐴 ((𝑔𝑘) ∩ 𝑆) → X𝑘𝐴 ((𝑔𝑘) ∩ 𝑆) ≠ ∅)
106 vex 3479 . . . . . . . . . . . . . . . . 17 ∈ V
107106elixp 8894 . . . . . . . . . . . . . . . 16 (X𝑘𝐴 ((𝑔𝑘) ∩ 𝑆) ↔ ( Fn 𝐴 ∧ ∀𝑘𝐴 (𝑘) ∈ ((𝑔𝑘) ∩ 𝑆)))
108 ixpin 8913 . . . . . . . . . . . . . . . . . 18 X𝑘𝐴 ((𝑔𝑘) ∩ 𝑆) = (X𝑘𝐴 (𝑔𝑘) ∩ X𝑘𝐴 𝑆)
10961ineq1i 4207 . . . . . . . . . . . . . . . . . 18 (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) = (X𝑘𝐴 (𝑔𝑘) ∩ X𝑘𝐴 𝑆)
110108, 109eqtr4i 2764 . . . . . . . . . . . . . . . . 17 X𝑘𝐴 ((𝑔𝑘) ∩ 𝑆) = (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆)
111110neeq1i 3006 . . . . . . . . . . . . . . . 16 (X𝑘𝐴 ((𝑔𝑘) ∩ 𝑆) ≠ ∅ ↔ (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅)
112105, 107, 1113imtr3i 291 . . . . . . . . . . . . . . 15 (( Fn 𝐴 ∧ ∀𝑘𝐴 (𝑘) ∈ ((𝑔𝑘) ∩ 𝑆)) → (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅)
113104, 112sylan2br 596 . . . . . . . . . . . . . 14 (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)) → (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅)
11499, 113sylan 581 . . . . . . . . . . . . 13 ((:𝐴 𝑘𝐴 𝑆 ∧ ∀𝑦𝐴 (𝑦) ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)) → (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅)
115114exlimiv 1934 . . . . . . . . . . . 12 (∃(:𝐴 𝑘𝐴 𝑆 ∧ ∀𝑦𝐴 (𝑦) ∈ ((𝑔𝑦) ∩ 𝑦 / 𝑘𝑆)) → (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅)
11698, 115syl 17 . . . . . . . . . . 11 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ ((𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅) ∧ 𝑓X𝑦𝐴 (𝑔𝑦))) → (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅)
117116expr 458 . . . . . . . . . 10 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑔𝑘) ∈ 𝑅)) → (𝑓X𝑦𝐴 (𝑔𝑦) → (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅))
11845, 117syldan 592 . . . . . . . . 9 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦))) → (𝑓X𝑦𝐴 (𝑔𝑦) → (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅))
1191183adantr3 1172 . . . . . . . 8 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦))) → (𝑓X𝑦𝐴 (𝑔𝑦) → (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅))
120 eleq2 2823 . . . . . . . . 9 (𝑢 = X𝑦𝐴 (𝑔𝑦) → (𝑓𝑢𝑓X𝑦𝐴 (𝑔𝑦)))
121 ineq1 4204 . . . . . . . . . 10 (𝑢 = X𝑦𝐴 (𝑔𝑦) → (𝑢X𝑘𝐴 𝑆) = (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆))
122121neeq1d 3001 . . . . . . . . 9 (𝑢 = X𝑦𝐴 (𝑔𝑦) → ((𝑢X𝑘𝐴 𝑆) ≠ ∅ ↔ (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅))
123120, 122imbi12d 345 . . . . . . . 8 (𝑢 = X𝑦𝐴 (𝑔𝑦) → ((𝑓𝑢 → (𝑢X𝑘𝐴 𝑆) ≠ ∅) ↔ (𝑓X𝑦𝐴 (𝑔𝑦) → (X𝑦𝐴 (𝑔𝑦) ∩ X𝑘𝐴 𝑆) ≠ ∅)))
124119, 123syl5ibrcom 246 . . . . . . 7 (((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) ∧ (𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦))) → (𝑢 = X𝑦𝐴 (𝑔𝑦) → (𝑓𝑢 → (𝑢X𝑘𝐴 𝑆) ≠ ∅)))
125124expimpd 455 . . . . . 6 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → (((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑢 = X𝑦𝐴 (𝑔𝑦)) → (𝑓𝑢 → (𝑢X𝑘𝐴 𝑆) ≠ ∅)))
126125exlimdv 1937 . . . . 5 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → (∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑢 = X𝑦𝐴 (𝑔𝑦)) → (𝑓𝑢 → (𝑢X𝑘𝐴 𝑆) ≠ ∅)))
12728, 126biimtrid 241 . . . 4 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → (𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} → (𝑓𝑢 → (𝑢X𝑘𝐴 𝑆) ≠ ∅)))
128127ralrimiv 3146 . . 3 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → ∀𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} (𝑓𝑢 → (𝑢X𝑘𝐴 𝑆) ≠ ∅))
1294fmpttd 7110 . . . . . . . 8 (𝜑 → (𝑘𝐴𝑅):𝐴⟶Top)
130129ffnd 6715 . . . . . . 7 (𝜑 → (𝑘𝐴𝑅) Fn 𝐴)
131 eqid 2733 . . . . . . . 8 {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}
132131ptval 23056 . . . . . . 7 ((𝐴𝑉 ∧ (𝑘𝐴𝑅) Fn 𝐴) → (∏t‘(𝑘𝐴𝑅)) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}))
1331, 130, 132syl2anc 585 . . . . . 6 (𝜑 → (∏t‘(𝑘𝐴𝑅)) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}))
13413, 133eqtrid 2785 . . . . 5 (𝜑𝐽 = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}))
135134adantr 482 . . . 4 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → 𝐽 = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}))
1362ralrimiva 3147 . . . . . . 7 (𝜑 → ∀𝑘𝐴 𝑅 ∈ (TopOn‘𝑋))
13713pttopon 23082 . . . . . . 7 ((𝐴𝑉 ∧ ∀𝑘𝐴 𝑅 ∈ (TopOn‘𝑋)) → 𝐽 ∈ (TopOn‘X𝑘𝐴 𝑋))
1381, 136, 137syl2anc 585 . . . . . 6 (𝜑𝐽 ∈ (TopOn‘X𝑘𝐴 𝑋))
139 toponuni 22398 . . . . . 6 (𝐽 ∈ (TopOn‘X𝑘𝐴 𝑋) → X𝑘𝐴 𝑋 = 𝐽)
140138, 139syl 17 . . . . 5 (𝜑X𝑘𝐴 𝑋 = 𝐽)
141140adantr 482 . . . 4 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → X𝑘𝐴 𝑋 = 𝐽)
142131ptbas 23065 . . . . . 6 ((𝐴𝑉 ∧ (𝑘𝐴𝑅):𝐴⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} ∈ TopBases)
1431, 129, 142syl2anc 585 . . . . 5 (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} ∈ TopBases)
144143adantr 482 . . . 4 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} ∈ TopBases)
1455ralrimiva 3147 . . . . . 6 (𝜑 → ∀𝑘𝐴 𝑆𝑋)
146 ss2ixp 8900 . . . . . 6 (∀𝑘𝐴 𝑆𝑋X𝑘𝐴 𝑆X𝑘𝐴 𝑋)
147145, 146syl 17 . . . . 5 (𝜑X𝑘𝐴 𝑆X𝑘𝐴 𝑋)
148147adantr 482 . . . 4 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → X𝑘𝐴 𝑆X𝑘𝐴 𝑋)
1499clsss3 22545 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 𝑅) → ((cls‘𝑅)‘𝑆) ⊆ 𝑅)
1504, 8, 149syl2anc 585 . . . . . . . 8 ((𝜑𝑘𝐴) → ((cls‘𝑅)‘𝑆) ⊆ 𝑅)
151150, 7sseqtrrd 4022 . . . . . . 7 ((𝜑𝑘𝐴) → ((cls‘𝑅)‘𝑆) ⊆ 𝑋)
152151ralrimiva 3147 . . . . . 6 (𝜑 → ∀𝑘𝐴 ((cls‘𝑅)‘𝑆) ⊆ 𝑋)
153 ss2ixp 8900 . . . . . 6 (∀𝑘𝐴 ((cls‘𝑅)‘𝑆) ⊆ 𝑋X𝑘𝐴 ((cls‘𝑅)‘𝑆) ⊆ X𝑘𝐴 𝑋)
154152, 153syl 17 . . . . 5 (𝜑X𝑘𝐴 ((cls‘𝑅)‘𝑆) ⊆ X𝑘𝐴 𝑋)
155154sselda 3981 . . . 4 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → 𝑓X𝑘𝐴 𝑋)
156135, 141, 144, 148, 155elcls3 22569 . . 3 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → (𝑓 ∈ ((cls‘𝐽)‘X𝑘𝐴 𝑆) ↔ ∀𝑢 ∈ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ ((𝑘𝐴𝑅)‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = ((𝑘𝐴𝑅)‘𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))} (𝑓𝑢 → (𝑢X𝑘𝐴 𝑆) ≠ ∅)))
157128, 156mpbird 257 . 2 ((𝜑𝑓X𝑘𝐴 ((cls‘𝑅)‘𝑆)) → 𝑓 ∈ ((cls‘𝐽)‘X𝑘𝐴 𝑆))
15823, 157eqelssd 4002 1 (𝜑 → ((cls‘𝐽)‘X𝑘𝐴 𝑆) = X𝑘𝐴 ((cls‘𝑅)‘𝑆))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wex 1782  wcel 2107  {cab 2710  wne 2941  wral 3062  wrex 3071  {crab 3433  csb 3892  cdif 3944  cin 3946  wss 3947  c0 4321   cuni 4907   ciun 4996  cmpt 5230   Fn wfn 6535  wf 6536  cfv 6540  Xcixp 8887  Fincfn 8935  AC wacn 9929  topGenctg 17379  tcpt 17380  Topctop 22377  TopOnctopon 22394  TopBasesctb 22430  Clsdccld 22502  clsccl 22504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-oprab 7408  df-mpo 7409  df-om 7851  df-1o 8461  df-er 8699  df-map 8818  df-ixp 8888  df-en 8936  df-fin 8939  df-fi 9402  df-acn 9933  df-topgen 17385  df-pt 17386  df-top 22378  df-topon 22395  df-bases 22431  df-cld 22505  df-ntr 22506  df-cls 22507
This theorem is referenced by:  ptcls  23102  dfac14  23104
  Copyright terms: Public domain W3C validator