Metamath Proof Explorer


Theorem ptclsg

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)

Ref Expression
Hypotheses ptcls.2 𝐽 = ( ∏t ‘ ( 𝑘𝐴𝑅 ) )
ptcls.a ( 𝜑𝐴𝑉 )
ptcls.j ( ( 𝜑𝑘𝐴 ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
ptcls.c ( ( 𝜑𝑘𝐴 ) → 𝑆𝑋 )
ptclsg.1 ( 𝜑 𝑘𝐴 𝑆AC 𝐴 )
Assertion ptclsg ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ X 𝑘𝐴 𝑆 ) = X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ptcls.2 𝐽 = ( ∏t ‘ ( 𝑘𝐴𝑅 ) )
2 ptcls.a ( 𝜑𝐴𝑉 )
3 ptcls.j ( ( 𝜑𝑘𝐴 ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
4 ptcls.c ( ( 𝜑𝑘𝐴 ) → 𝑆𝑋 )
5 ptclsg.1 ( 𝜑 𝑘𝐴 𝑆AC 𝐴 )
6 topontop ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑅 ∈ Top )
7 3 6 syl ( ( 𝜑𝑘𝐴 ) → 𝑅 ∈ Top )
8 toponuni ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝑅 )
9 3 8 syl ( ( 𝜑𝑘𝐴 ) → 𝑋 = 𝑅 )
10 4 9 sseqtrd ( ( 𝜑𝑘𝐴 ) → 𝑆 𝑅 )
11 eqid 𝑅 = 𝑅
12 11 clscld ( ( 𝑅 ∈ Top ∧ 𝑆 𝑅 ) → ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝑅 ) )
13 7 10 12 syl2anc ( ( 𝜑𝑘𝐴 ) → ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝑅 ) )
14 2 7 13 ptcldmpt ( 𝜑X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ∈ ( Clsd ‘ ( ∏t ‘ ( 𝑘𝐴𝑅 ) ) ) )
15 1 fveq2i ( Clsd ‘ 𝐽 ) = ( Clsd ‘ ( ∏t ‘ ( 𝑘𝐴𝑅 ) ) )
16 14 15 eleqtrrdi ( 𝜑X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
17 11 sscls ( ( 𝑅 ∈ Top ∧ 𝑆 𝑅 ) → 𝑆 ⊆ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
18 7 10 17 syl2anc ( ( 𝜑𝑘𝐴 ) → 𝑆 ⊆ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
19 18 ralrimiva ( 𝜑 → ∀ 𝑘𝐴 𝑆 ⊆ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
20 ss2ixp ( ∀ 𝑘𝐴 𝑆 ⊆ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) → X 𝑘𝐴 𝑆X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
21 19 20 syl ( 𝜑X 𝑘𝐴 𝑆X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
22 eqid 𝐽 = 𝐽
23 22 clsss2 ( ( X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) ∧ X 𝑘𝐴 𝑆X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → ( ( cls ‘ 𝐽 ) ‘ X 𝑘𝐴 𝑆 ) ⊆ X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
24 16 21 23 syl2anc ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ X 𝑘𝐴 𝑆 ) ⊆ X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
25 vex 𝑢 ∈ V
26 eqeq1 ( 𝑥 = 𝑢 → ( 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ↔ 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) ) )
27 26 anbi2d ( 𝑥 = 𝑢 → ( ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) ↔ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) ) ) )
28 27 exbidv ( 𝑥 = 𝑢 → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) ) ) )
29 25 28 elab ( 𝑢 ∈ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ↔ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) ) )
30 nffvmpt1 𝑘 ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 )
31 30 nfel2 𝑘 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 )
32 nfv 𝑦 ( 𝑔𝑘 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑘 )
33 fveq2 ( 𝑦 = 𝑘 → ( 𝑔𝑦 ) = ( 𝑔𝑘 ) )
34 fveq2 ( 𝑦 = 𝑘 → ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑘 ) )
35 33 34 eleq12d ( 𝑦 = 𝑘 → ( ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ↔ ( 𝑔𝑘 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑘 ) ) )
36 31 32 35 cbvralw ( ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ↔ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑘 ) )
37 simpr ( ( 𝜑𝑘𝐴 ) → 𝑘𝐴 )
38 eqid ( 𝑘𝐴𝑅 ) = ( 𝑘𝐴𝑅 )
39 38 fvmpt2 ( ( 𝑘𝐴𝑅 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( 𝑘𝐴𝑅 ) ‘ 𝑘 ) = 𝑅 )
40 37 3 39 syl2anc ( ( 𝜑𝑘𝐴 ) → ( ( 𝑘𝐴𝑅 ) ‘ 𝑘 ) = 𝑅 )
41 40 eleq2d ( ( 𝜑𝑘𝐴 ) → ( ( 𝑔𝑘 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑘 ) ↔ ( 𝑔𝑘 ) ∈ 𝑅 ) )
42 41 ralbidva ( 𝜑 → ( ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑘 ) ↔ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) )
43 36 42 syl5bb ( 𝜑 → ( ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ↔ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) )
44 43 anbi2d ( 𝜑 → ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ↔ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ) )
45 44 adantr ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ↔ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ) )
46 45 biimpa ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ) → ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) )
47 5 ad2antrr ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → 𝑘𝐴 𝑆AC 𝐴 )
48 simpll ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → 𝜑 )
49 vex 𝑓 ∈ V
50 49 elixp ( 𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) )
51 50 simprbi ( 𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) → ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
52 51 ad2antlr ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )
53 11 clsndisj ( ( ( 𝑅 ∈ Top ∧ 𝑆 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔𝑘 ) ∈ 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) ) → ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ )
54 53 ex ( ( 𝑅 ∈ Top ∧ 𝑆 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → ( ( ( 𝑔𝑘 ) ∈ 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) → ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ ) )
55 54 3expia ( ( 𝑅 ∈ Top ∧ 𝑆 𝑅 ) → ( ( 𝑓𝑘 ) ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) → ( ( ( 𝑔𝑘 ) ∈ 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) → ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ ) ) )
56 7 10 55 syl2anc ( ( 𝜑𝑘𝐴 ) → ( ( 𝑓𝑘 ) ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) → ( ( ( 𝑔𝑘 ) ∈ 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) → ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ ) ) )
57 56 ralimdva ( 𝜑 → ( ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) → ∀ 𝑘𝐴 ( ( ( 𝑔𝑘 ) ∈ 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) → ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ ) ) )
58 48 52 57 sylc ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → ∀ 𝑘𝐴 ( ( ( 𝑔𝑘 ) ∈ 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) → ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ ) )
59 simprlr ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 )
60 simprr ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) )
61 33 cbvixpv X 𝑦𝐴 ( 𝑔𝑦 ) = X 𝑘𝐴 ( 𝑔𝑘 )
62 60 61 eleqtrdi ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → 𝑓X 𝑘𝐴 ( 𝑔𝑘 ) )
63 49 elixp ( 𝑓X 𝑘𝐴 ( 𝑔𝑘 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) )
64 63 simprbi ( 𝑓X 𝑘𝐴 ( 𝑔𝑘 ) → ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) )
65 62 64 syl ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) )
66 r19.26 ( ∀ 𝑘𝐴 ( ( 𝑔𝑘 ) ∈ 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) ↔ ( ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ∧ ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) )
67 59 65 66 sylanbrc ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → ∀ 𝑘𝐴 ( ( 𝑔𝑘 ) ∈ 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) )
68 ralim ( ∀ 𝑘𝐴 ( ( ( 𝑔𝑘 ) ∈ 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) → ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ ) → ( ∀ 𝑘𝐴 ( ( 𝑔𝑘 ) ∈ 𝑅 ∧ ( 𝑓𝑘 ) ∈ ( 𝑔𝑘 ) ) → ∀ 𝑘𝐴 ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ ) )
69 58 67 68 sylc ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → ∀ 𝑘𝐴 ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ )
70 rabn0 ( { 𝑧 𝑘𝐴 𝑆𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) } ≠ ∅ ↔ ∃ 𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) )
71 dfin5 ( 𝑘𝐴 𝑆 ∩ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ) = { 𝑧 𝑘𝐴 𝑆𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) }
72 inss2 ( ( 𝑔𝑘 ) ∩ 𝑆 ) ⊆ 𝑆
73 ssiun2 ( 𝑘𝐴𝑆 𝑘𝐴 𝑆 )
74 72 73 sstrid ( 𝑘𝐴 → ( ( 𝑔𝑘 ) ∩ 𝑆 ) ⊆ 𝑘𝐴 𝑆 )
75 sseqin2 ( ( ( 𝑔𝑘 ) ∩ 𝑆 ) ⊆ 𝑘𝐴 𝑆 ↔ ( 𝑘𝐴 𝑆 ∩ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ) = ( ( 𝑔𝑘 ) ∩ 𝑆 ) )
76 74 75 sylib ( 𝑘𝐴 → ( 𝑘𝐴 𝑆 ∩ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ) = ( ( 𝑔𝑘 ) ∩ 𝑆 ) )
77 71 76 eqtr3id ( 𝑘𝐴 → { 𝑧 𝑘𝐴 𝑆𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) } = ( ( 𝑔𝑘 ) ∩ 𝑆 ) )
78 77 neeq1d ( 𝑘𝐴 → ( { 𝑧 𝑘𝐴 𝑆𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) } ≠ ∅ ↔ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ ) )
79 70 78 bitr3id ( 𝑘𝐴 → ( ∃ 𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ↔ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ ) )
80 79 ralbiia ( ∀ 𝑘𝐴𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ↔ ∀ 𝑘𝐴 ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ )
81 69 80 sylibr ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → ∀ 𝑘𝐴𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) )
82 nfv 𝑦𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 )
83 nfiu1 𝑘 𝑘𝐴 𝑆
84 nfcv 𝑘 ( 𝑔𝑦 )
85 nfcsb1v 𝑘 𝑦 / 𝑘 𝑆
86 84 85 nfin 𝑘 ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 )
87 86 nfel2 𝑘 𝑧 ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 )
88 83 87 nfrex 𝑘𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 )
89 fveq2 ( 𝑘 = 𝑦 → ( 𝑔𝑘 ) = ( 𝑔𝑦 ) )
90 csbeq1a ( 𝑘 = 𝑦𝑆 = 𝑦 / 𝑘 𝑆 )
91 89 90 ineq12d ( 𝑘 = 𝑦 → ( ( 𝑔𝑘 ) ∩ 𝑆 ) = ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) )
92 91 eleq2d ( 𝑘 = 𝑦 → ( 𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ↔ 𝑧 ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ) )
93 92 rexbidv ( 𝑘 = 𝑦 → ( ∃ 𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ↔ ∃ 𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ) )
94 82 88 93 cbvralw ( ∀ 𝑘𝐴𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ↔ ∀ 𝑦𝐴𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) )
95 81 94 sylib ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → ∀ 𝑦𝐴𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) )
96 eleq1 ( 𝑧 = ( 𝑦 ) → ( 𝑧 ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ↔ ( 𝑦 ) ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ) )
97 96 acni3 ( ( 𝑘𝐴 𝑆AC 𝐴 ∧ ∀ 𝑦𝐴𝑧 𝑘𝐴 𝑆 𝑧 ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ) → ∃ ( : 𝐴 𝑘𝐴 𝑆 ∧ ∀ 𝑦𝐴 ( 𝑦 ) ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ) )
98 47 95 97 syl2anc ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → ∃ ( : 𝐴 𝑘𝐴 𝑆 ∧ ∀ 𝑦𝐴 ( 𝑦 ) ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ) )
99 ffn ( : 𝐴 𝑘𝐴 𝑆 Fn 𝐴 )
100 nfv 𝑦 ( 𝑘 ) ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 )
101 86 nfel2 𝑘 ( 𝑦 ) ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 )
102 fveq2 ( 𝑘 = 𝑦 → ( 𝑘 ) = ( 𝑦 ) )
103 102 91 eleq12d ( 𝑘 = 𝑦 → ( ( 𝑘 ) ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ↔ ( 𝑦 ) ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ) )
104 100 101 103 cbvralw ( ∀ 𝑘𝐴 ( 𝑘 ) ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ↔ ∀ 𝑦𝐴 ( 𝑦 ) ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) )
105 ne0i ( X 𝑘𝐴 ( ( 𝑔𝑘 ) ∩ 𝑆 ) → X 𝑘𝐴 ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ )
106 vex ∈ V
107 106 elixp ( X 𝑘𝐴 ( ( 𝑔𝑘 ) ∩ 𝑆 ) ↔ ( Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑘 ) ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ) )
108 ixpin X 𝑘𝐴 ( ( 𝑔𝑘 ) ∩ 𝑆 ) = ( X 𝑘𝐴 ( 𝑔𝑘 ) ∩ X 𝑘𝐴 𝑆 )
109 61 ineq1i ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) = ( X 𝑘𝐴 ( 𝑔𝑘 ) ∩ X 𝑘𝐴 𝑆 )
110 108 109 eqtr4i X 𝑘𝐴 ( ( 𝑔𝑘 ) ∩ 𝑆 ) = ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 )
111 110 neeq1i ( X 𝑘𝐴 ( ( 𝑔𝑘 ) ∩ 𝑆 ) ≠ ∅ ↔ ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ )
112 105 107 111 3imtr3i ( ( Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑘 ) ∈ ( ( 𝑔𝑘 ) ∩ 𝑆 ) ) → ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ )
113 104 112 sylan2br ( ( Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑦 ) ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ) → ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ )
114 99 113 sylan ( ( : 𝐴 𝑘𝐴 𝑆 ∧ ∀ 𝑦𝐴 ( 𝑦 ) ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ) → ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ )
115 114 exlimiv ( ∃ ( : 𝐴 𝑘𝐴 𝑆 ∧ ∀ 𝑦𝐴 ( 𝑦 ) ∈ ( ( 𝑔𝑦 ) ∩ 𝑦 / 𝑘 𝑆 ) ) → ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ )
116 98 115 syl ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ∧ 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) ) → ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ )
117 116 expr ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑔𝑘 ) ∈ 𝑅 ) ) → ( 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) → ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ ) )
118 46 117 syldan ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ) → ( 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) → ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ ) )
119 118 3adantr3 ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ) → ( 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) → ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ ) )
120 eleq2 ( 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) → ( 𝑓𝑢𝑓X 𝑦𝐴 ( 𝑔𝑦 ) ) )
121 ineq1 ( 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) → ( 𝑢X 𝑘𝐴 𝑆 ) = ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) )
122 121 neeq1d ( 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) → ( ( 𝑢X 𝑘𝐴 𝑆 ) ≠ ∅ ↔ ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ ) )
123 120 122 imbi12d ( 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) → ( ( 𝑓𝑢 → ( 𝑢X 𝑘𝐴 𝑆 ) ≠ ∅ ) ↔ ( 𝑓X 𝑦𝐴 ( 𝑔𝑦 ) → ( X 𝑦𝐴 ( 𝑔𝑦 ) ∩ X 𝑘𝐴 𝑆 ) ≠ ∅ ) ) )
124 119 123 syl5ibrcom ( ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) ∧ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ) → ( 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) → ( 𝑓𝑢 → ( 𝑢X 𝑘𝐴 𝑆 ) ≠ ∅ ) ) )
125 124 expimpd ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → ( ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) ) → ( 𝑓𝑢 → ( 𝑢X 𝑘𝐴 𝑆 ) ≠ ∅ ) ) )
126 125 exlimdv ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → ( ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑢 = X 𝑦𝐴 ( 𝑔𝑦 ) ) → ( 𝑓𝑢 → ( 𝑢X 𝑘𝐴 𝑆 ) ≠ ∅ ) ) )
127 29 126 syl5bi ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → ( 𝑢 ∈ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } → ( 𝑓𝑢 → ( 𝑢X 𝑘𝐴 𝑆 ) ≠ ∅ ) ) )
128 127 ralrimiv ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → ∀ 𝑢 ∈ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ( 𝑓𝑢 → ( 𝑢X 𝑘𝐴 𝑆 ) ≠ ∅ ) )
129 7 fmpttd ( 𝜑 → ( 𝑘𝐴𝑅 ) : 𝐴 ⟶ Top )
130 129 ffnd ( 𝜑 → ( 𝑘𝐴𝑅 ) Fn 𝐴 )
131 eqid { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } = { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) }
132 131 ptval ( ( 𝐴𝑉 ∧ ( 𝑘𝐴𝑅 ) Fn 𝐴 ) → ( ∏t ‘ ( 𝑘𝐴𝑅 ) ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
133 2 130 132 syl2anc ( 𝜑 → ( ∏t ‘ ( 𝑘𝐴𝑅 ) ) = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
134 1 133 eqtrid ( 𝜑𝐽 = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
135 134 adantr ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → 𝐽 = ( topGen ‘ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
136 3 ralrimiva ( 𝜑 → ∀ 𝑘𝐴 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
137 1 pttopon ( ( 𝐴𝑉 ∧ ∀ 𝑘𝐴 𝑅 ∈ ( TopOn ‘ 𝑋 ) ) → 𝐽 ∈ ( TopOn ‘ X 𝑘𝐴 𝑋 ) )
138 2 136 137 syl2anc ( 𝜑𝐽 ∈ ( TopOn ‘ X 𝑘𝐴 𝑋 ) )
139 toponuni ( 𝐽 ∈ ( TopOn ‘ X 𝑘𝐴 𝑋 ) → X 𝑘𝐴 𝑋 = 𝐽 )
140 138 139 syl ( 𝜑X 𝑘𝐴 𝑋 = 𝐽 )
141 140 adantr ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → X 𝑘𝐴 𝑋 = 𝐽 )
142 131 ptbas ( ( 𝐴𝑉 ∧ ( 𝑘𝐴𝑅 ) : 𝐴 ⟶ Top ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ∈ TopBases )
143 2 129 142 syl2anc ( 𝜑 → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ∈ TopBases )
144 143 adantr ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ∈ TopBases )
145 4 ralrimiva ( 𝜑 → ∀ 𝑘𝐴 𝑆𝑋 )
146 ss2ixp ( ∀ 𝑘𝐴 𝑆𝑋X 𝑘𝐴 𝑆X 𝑘𝐴 𝑋 )
147 145 146 syl ( 𝜑X 𝑘𝐴 𝑆X 𝑘𝐴 𝑋 )
148 147 adantr ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → X 𝑘𝐴 𝑆X 𝑘𝐴 𝑋 )
149 11 clsss3 ( ( 𝑅 ∈ Top ∧ 𝑆 𝑅 ) → ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ⊆ 𝑅 )
150 7 10 149 syl2anc ( ( 𝜑𝑘𝐴 ) → ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ⊆ 𝑅 )
151 150 9 sseqtrrd ( ( 𝜑𝑘𝐴 ) → ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ⊆ 𝑋 )
152 151 ralrimiva ( 𝜑 → ∀ 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ⊆ 𝑋 )
153 ss2ixp ( ∀ 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ⊆ 𝑋X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ⊆ X 𝑘𝐴 𝑋 )
154 152 153 syl ( 𝜑X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ⊆ X 𝑘𝐴 𝑋 )
155 154 sselda ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → 𝑓X 𝑘𝐴 𝑋 )
156 135 141 144 148 155 elcls3 ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → ( 𝑓 ∈ ( ( cls ‘ 𝐽 ) ‘ X 𝑘𝐴 𝑆 ) ↔ ∀ 𝑢 ∈ { 𝑥 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( ( 𝑘𝐴𝑅 ) ‘ 𝑦 ) ) ∧ 𝑥 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ( 𝑓𝑢 → ( 𝑢X 𝑘𝐴 𝑆 ) ≠ ∅ ) ) )
157 128 156 mpbird ( ( 𝜑𝑓X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) ) → 𝑓 ∈ ( ( cls ‘ 𝐽 ) ‘ X 𝑘𝐴 𝑆 ) )
158 24 157 eqelssd ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ X 𝑘𝐴 𝑆 ) = X 𝑘𝐴 ( ( cls ‘ 𝑅 ) ‘ 𝑆 ) )