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 syl5eq ⊢ ( 𝜑 → 𝐽 = ( 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 ‘ 𝑅 ) ‘ 𝑆 ) )