MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ptclsg Structured version   Visualization version   GIF version
Theorem ptclsg 23119
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 22415 . . . . . 6 (𝑅 ∈ (TopOnβ€˜π‘‹) β†’ 𝑅 ∈ Top)
42, 3syl 17 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑅 ∈ Top)
5 ptcls.c . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑆 βŠ† 𝑋)
6 toponuni 22416 . . . . . . . 8 (𝑅 ∈ (TopOnβ€˜π‘‹) β†’ 𝑋 = βˆͺ 𝑅)
72, 6syl 17 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑋 = βˆͺ 𝑅)
85, 7sseqtrd 4023 . . . . . 6 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑆 βŠ† βˆͺ 𝑅)
9 eqid 2733 . . . . . . 7 βˆͺ 𝑅 = βˆͺ 𝑅
109clscld 22551 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 βŠ† βˆͺ 𝑅) β†’ ((clsβ€˜π‘…)β€˜π‘†) ∈ (Clsdβ€˜π‘…))
114, 8, 10syl2anc 585 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ ((clsβ€˜π‘…)β€˜π‘†) ∈ (Clsdβ€˜π‘…))
121, 4, 11ptcldmpt 23118 . . . 4 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†) ∈ (Clsdβ€˜(∏tβ€˜(π‘˜ ∈ 𝐴 ↦ 𝑅))))
13 ptcls.2 . . . . 5 𝐽 = (∏tβ€˜(π‘˜ ∈ 𝐴 ↦ 𝑅))
1413fveq2i 6895 . . . 4 (Clsdβ€˜π½) = (Clsdβ€˜(∏tβ€˜(π‘˜ ∈ 𝐴 ↦ 𝑅)))
1512, 14eleqtrrdi 2845 . . 3 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†) ∈ (Clsdβ€˜π½))
169sscls 22560 . . . . . 6 ((𝑅 ∈ Top ∧ 𝑆 βŠ† βˆͺ 𝑅) β†’ 𝑆 βŠ† ((clsβ€˜π‘…)β€˜π‘†))
174, 8, 16syl2anc 585 . . . . 5 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ 𝑆 βŠ† ((clsβ€˜π‘…)β€˜π‘†))
1817ralrimiva 3147 . . . 4 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐴 𝑆 βŠ† ((clsβ€˜π‘…)β€˜π‘†))
19 ss2ixp 8904 . . . 4 (βˆ€π‘˜ ∈ 𝐴 𝑆 βŠ† ((clsβ€˜π‘…)β€˜π‘†) β†’ Xπ‘˜ ∈ 𝐴 𝑆 βŠ† Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†))
2018, 19syl 17 . . 3 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 𝑆 βŠ† Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†))
21 eqid 2733 . . . 4 βˆͺ 𝐽 = βˆͺ 𝐽
2221clsss2 22576 . . 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 3669 . . . . 5 (𝑒 ∈ {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝐴 ∧ βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝐴 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝐴 (π‘”β€˜π‘¦))} ↔ βˆƒπ‘”((𝑔 Fn 𝐴 ∧ βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝐴 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦)) ∧ 𝑒 = X𝑦 ∈ 𝐴 (π‘”β€˜π‘¦)))
29 nffvmpt1 6903 . . . . . . . . . . . . . . . 16 β„²π‘˜((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦)
3029nfel2 2922 . . . . . . . . . . . . . . 15 β„²π‘˜(π‘”β€˜π‘¦) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦)
31 nfv 1918 . . . . . . . . . . . . . . 15 Ⅎ𝑦(π‘”β€˜π‘˜) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘˜)
32 fveq2 6892 . . . . . . . . . . . . . . . 16 (𝑦 = π‘˜ β†’ (π‘”β€˜π‘¦) = (π‘”β€˜π‘˜))
33 fveq2 6892 . . . . . . . . . . . . . . . 16 (𝑦 = π‘˜ β†’ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦) = ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘˜))
3432, 33eleq12d 2828 . . . . . . . . . . . . . . 15 (𝑦 = π‘˜ β†’ ((π‘”β€˜π‘¦) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦) ↔ (π‘”β€˜π‘˜) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘˜)))
3530, 31, 34cbvralw 3304 . . . . . . . . . . . . . 14 (βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦) ↔ βˆ€π‘˜ ∈ 𝐴 (π‘”β€˜π‘˜) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘˜))
36 simpr 486 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ π‘˜ ∈ 𝐴)
37 eqid 2733 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ 𝐴 ↦ 𝑅) = (π‘˜ ∈ 𝐴 ↦ 𝑅)
3837fvmpt2 7010 . . . . . . . . . . . . . . . . 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 8898 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†) ↔ (𝑓 Fn 𝐴 ∧ βˆ€π‘˜ ∈ 𝐴 (π‘“β€˜π‘˜) ∈ ((clsβ€˜π‘…)β€˜π‘†)))
5150simprbi 498 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†) β†’ βˆ€π‘˜ ∈ 𝐴 (π‘“β€˜π‘˜) ∈ ((clsβ€˜π‘…)β€˜π‘†))
5251ad2antlr 726 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†)) ∧ ((𝑔 Fn 𝐴 ∧ βˆ€π‘˜ ∈ 𝐴 (π‘”β€˜π‘˜) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (π‘”β€˜π‘¦))) β†’ βˆ€π‘˜ ∈ 𝐴 (π‘“β€˜π‘˜) ∈ ((clsβ€˜π‘…)β€˜π‘†))
539clsndisj 22579 . . . . . . . . . . . . . . . . . . . . 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 8909 . . . . . . . . . . . . . . . . . . 19 X𝑦 ∈ 𝐴 (π‘”β€˜π‘¦) = Xπ‘˜ ∈ 𝐴 (π‘”β€˜π‘˜)
6260, 61eleqtrdi 2844 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†)) ∧ ((𝑔 Fn 𝐴 ∧ βˆ€π‘˜ ∈ 𝐴 (π‘”β€˜π‘˜) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (π‘”β€˜π‘¦))) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝐴 (π‘”β€˜π‘˜))
6349elixp 8898 . . . . . . . . . . . . . . . . . . 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 4386 . . . . . . . . . . . . . . . . 17 ({𝑧 ∈ βˆͺ π‘˜ ∈ 𝐴 𝑆 ∣ 𝑧 ∈ ((π‘”β€˜π‘˜) ∩ 𝑆)} β‰  βˆ… ↔ βˆƒπ‘§ ∈ βˆͺ π‘˜ ∈ 𝐴 𝑆𝑧 ∈ ((π‘”β€˜π‘˜) ∩ 𝑆))
71 dfin5 3957 . . . . . . . . . . . . . . . . . . 19 (βˆͺ π‘˜ ∈ 𝐴 𝑆 ∩ ((π‘”β€˜π‘˜) ∩ 𝑆)) = {𝑧 ∈ βˆͺ π‘˜ ∈ 𝐴 𝑆 ∣ 𝑧 ∈ ((π‘”β€˜π‘˜) ∩ 𝑆)}
72 inss2 4230 . . . . . . . . . . . . . . . . . . . . 21 ((π‘”β€˜π‘˜) ∩ 𝑆) βŠ† 𝑆
73 ssiun2 5051 . . . . . . . . . . . . . . . . . . . . 21 (π‘˜ ∈ 𝐴 β†’ 𝑆 βŠ† βˆͺ π‘˜ ∈ 𝐴 𝑆)
7472, 73sstrid 3994 . . . . . . . . . . . . . . . . . . . 20 (π‘˜ ∈ 𝐴 β†’ ((π‘”β€˜π‘˜) ∩ 𝑆) βŠ† βˆͺ π‘˜ ∈ 𝐴 𝑆)
75 sseqin2 4216 . . . . . . . . . . . . . . . . . . . 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 5032 . . . . . . . . . . . . . . . 16 β„²π‘˜βˆͺ π‘˜ ∈ 𝐴 𝑆
84 nfcv 2904 . . . . . . . . . . . . . . . . . 18 β„²π‘˜(π‘”β€˜π‘¦)
85 nfcsb1v 3919 . . . . . . . . . . . . . . . . . 18 β„²π‘˜β¦‹π‘¦ / π‘˜β¦Œπ‘†
8684, 85nfin 4217 . . . . . . . . . . . . . . . . 17 β„²π‘˜((π‘”β€˜π‘¦) ∩ ⦋𝑦 / π‘˜β¦Œπ‘†)
8786nfel2 2922 . . . . . . . . . . . . . . . 16 β„²π‘˜ 𝑧 ∈ ((π‘”β€˜π‘¦) ∩ ⦋𝑦 / π‘˜β¦Œπ‘†)
8883, 87nfrexw 3311 . . . . . . . . . . . . . . 15 β„²π‘˜βˆƒπ‘§ ∈ βˆͺ π‘˜ ∈ 𝐴 𝑆𝑧 ∈ ((π‘”β€˜π‘¦) ∩ ⦋𝑦 / π‘˜β¦Œπ‘†)
89 fveq2 6892 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑦 β†’ (π‘”β€˜π‘˜) = (π‘”β€˜π‘¦))
90 csbeq1a 3908 . . . . . . . . . . . . . . . . . 18 (π‘˜ = 𝑦 β†’ 𝑆 = ⦋𝑦 / π‘˜β¦Œπ‘†)
9189, 90ineq12d 4214 . . . . . . . . . . . . . . . . 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 10042 . . . . . . . . . . . . 13 ((βˆͺ π‘˜ ∈ 𝐴 𝑆 ∈ AC 𝐴 ∧ βˆ€π‘¦ ∈ 𝐴 βˆƒπ‘§ ∈ βˆͺ π‘˜ ∈ 𝐴 𝑆𝑧 ∈ ((π‘”β€˜π‘¦) ∩ ⦋𝑦 / π‘˜β¦Œπ‘†)) β†’ βˆƒβ„Ž(β„Ž:𝐴⟢βˆͺ π‘˜ ∈ 𝐴 𝑆 ∧ βˆ€π‘¦ ∈ 𝐴 (β„Žβ€˜π‘¦) ∈ ((π‘”β€˜π‘¦) ∩ ⦋𝑦 / π‘˜β¦Œπ‘†)))
9847, 95, 97syl2anc 585 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†)) ∧ ((𝑔 Fn 𝐴 ∧ βˆ€π‘˜ ∈ 𝐴 (π‘”β€˜π‘˜) ∈ 𝑅) ∧ 𝑓 ∈ X𝑦 ∈ 𝐴 (π‘”β€˜π‘¦))) β†’ βˆƒβ„Ž(β„Ž:𝐴⟢βˆͺ π‘˜ ∈ 𝐴 𝑆 ∧ βˆ€π‘¦ ∈ 𝐴 (β„Žβ€˜π‘¦) ∈ ((π‘”β€˜π‘¦) ∩ ⦋𝑦 / π‘˜β¦Œπ‘†)))
99 ffn 6718 . . . . . . . . . . . . . 14 (β„Ž:𝐴⟢βˆͺ π‘˜ ∈ 𝐴 𝑆 β†’ β„Ž Fn 𝐴)
100 nfv 1918 . . . . . . . . . . . . . . . 16 Ⅎ𝑦(β„Žβ€˜π‘˜) ∈ ((π‘”β€˜π‘˜) ∩ 𝑆)
10186nfel2 2922 . . . . . . . . . . . . . . . 16 β„²π‘˜(β„Žβ€˜π‘¦) ∈ ((π‘”β€˜π‘¦) ∩ ⦋𝑦 / π‘˜β¦Œπ‘†)
102 fveq2 6892 . . . . . . . . . . . . . . . . 17 (π‘˜ = 𝑦 β†’ (β„Žβ€˜π‘˜) = (β„Žβ€˜π‘¦))
103102, 91eleq12d 2828 . . . . . . . . . . . . . . . 16 (π‘˜ = 𝑦 β†’ ((β„Žβ€˜π‘˜) ∈ ((π‘”β€˜π‘˜) ∩ 𝑆) ↔ (β„Žβ€˜π‘¦) ∈ ((π‘”β€˜π‘¦) ∩ ⦋𝑦 / π‘˜β¦Œπ‘†)))
104100, 101, 103cbvralw 3304 . . . . . . . . . . . . . . 15 (βˆ€π‘˜ ∈ 𝐴 (β„Žβ€˜π‘˜) ∈ ((π‘”β€˜π‘˜) ∩ 𝑆) ↔ βˆ€π‘¦ ∈ 𝐴 (β„Žβ€˜π‘¦) ∈ ((π‘”β€˜π‘¦) ∩ ⦋𝑦 / π‘˜β¦Œπ‘†))
105 ne0i 4335 . . . . . . . . . . . . . . . 16 (β„Ž ∈ Xπ‘˜ ∈ 𝐴 ((π‘”β€˜π‘˜) ∩ 𝑆) β†’ Xπ‘˜ ∈ 𝐴 ((π‘”β€˜π‘˜) ∩ 𝑆) β‰  βˆ…)
106 vex 3479 . . . . . . . . . . . . . . . . 17 β„Ž ∈ V
107106elixp 8898 . . . . . . . . . . . . . . . 16 (β„Ž ∈ Xπ‘˜ ∈ 𝐴 ((π‘”β€˜π‘˜) ∩ 𝑆) ↔ (β„Ž Fn 𝐴 ∧ βˆ€π‘˜ ∈ 𝐴 (β„Žβ€˜π‘˜) ∈ ((π‘”β€˜π‘˜) ∩ 𝑆)))
108 ixpin 8917 . . . . . . . . . . . . . . . . . 18 Xπ‘˜ ∈ 𝐴 ((π‘”β€˜π‘˜) ∩ 𝑆) = (Xπ‘˜ ∈ 𝐴 (π‘”β€˜π‘˜) ∩ Xπ‘˜ ∈ 𝐴 𝑆)
10961ineq1i 4209 . . . . . . . . . . . . . . . . . 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 4206 . . . . . . . . . 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 7115 . . . . . . . 8 (πœ‘ β†’ (π‘˜ ∈ 𝐴 ↦ 𝑅):𝐴⟢Top)
130129ffnd 6719 . . . . . . 7 (πœ‘ β†’ (π‘˜ ∈ 𝐴 ↦ 𝑅) Fn 𝐴)
131 eqid 2733 . . . . . . . 8 {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝐴 ∧ βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝐴 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝐴 (π‘”β€˜π‘¦))} = {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝐴 ∧ βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝐴 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝐴 (π‘”β€˜π‘¦))}
132131ptval 23074 . . . . . . 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 23100 . . . . . . 7 ((𝐴 ∈ 𝑉 ∧ βˆ€π‘˜ ∈ 𝐴 𝑅 ∈ (TopOnβ€˜π‘‹)) β†’ 𝐽 ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐴 𝑋))
1381, 136, 137syl2anc 585 . . . . . 6 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐴 𝑋))
139 toponuni 22416 . . . . . 6 (𝐽 ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐴 𝑋) β†’ Xπ‘˜ ∈ 𝐴 𝑋 = βˆͺ 𝐽)
140138, 139syl 17 . . . . 5 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 𝑋 = βˆͺ 𝐽)
141140adantr 482 . . . 4 ((πœ‘ ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†)) β†’ Xπ‘˜ ∈ 𝐴 𝑋 = βˆͺ 𝐽)
142131ptbas 23083 . . . . . 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 8904 . . . . . 6 (βˆ€π‘˜ ∈ 𝐴 𝑆 βŠ† 𝑋 β†’ Xπ‘˜ ∈ 𝐴 𝑆 βŠ† Xπ‘˜ ∈ 𝐴 𝑋)
147145, 146syl 17 . . . . 5 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 𝑆 βŠ† Xπ‘˜ ∈ 𝐴 𝑋)
148147adantr 482 . . . 4 ((πœ‘ ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†)) β†’ Xπ‘˜ ∈ 𝐴 𝑆 βŠ† Xπ‘˜ ∈ 𝐴 𝑋)
1499clsss3 22563 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 βŠ† βˆͺ 𝑅) β†’ ((clsβ€˜π‘…)β€˜π‘†) βŠ† βˆͺ 𝑅)
1504, 8, 149syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ ((clsβ€˜π‘…)β€˜π‘†) βŠ† βˆͺ 𝑅)
151150, 7sseqtrrd 4024 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝐴) β†’ ((clsβ€˜π‘…)β€˜π‘†) βŠ† 𝑋)
152151ralrimiva 3147 . . . . . 6 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†) βŠ† 𝑋)
153 ss2ixp 8904 . . . . . 6 (βˆ€π‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†) βŠ† 𝑋 β†’ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†) βŠ† Xπ‘˜ ∈ 𝐴 𝑋)
154152, 153syl 17 . . . . 5 (πœ‘ β†’ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†) βŠ† Xπ‘˜ ∈ 𝐴 𝑋)
155154sselda 3983 . . . 4 ((πœ‘ ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†)) β†’ 𝑓 ∈ Xπ‘˜ ∈ 𝐴 𝑋)
156135, 141, 144, 148, 155elcls3 22587 . . 3 ((πœ‘ ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†)) β†’ (𝑓 ∈ ((clsβ€˜π½)β€˜Xπ‘˜ ∈ 𝐴 𝑆) ↔ βˆ€π‘’ ∈ {π‘₯ ∣ βˆƒπ‘”((𝑔 Fn 𝐴 ∧ βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) ∈ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦) ∧ βˆƒπ‘§ ∈ Fin βˆ€π‘¦ ∈ (𝐴 βˆ– 𝑧)(π‘”β€˜π‘¦) = βˆͺ ((π‘˜ ∈ 𝐴 ↦ 𝑅)β€˜π‘¦)) ∧ π‘₯ = X𝑦 ∈ 𝐴 (π‘”β€˜π‘¦))} (𝑓 ∈ 𝑒 β†’ (𝑒 ∩ Xπ‘˜ ∈ 𝐴 𝑆) β‰  βˆ…)))
157128, 156mpbird 257 . 2 ((πœ‘ ∧ 𝑓 ∈ Xπ‘˜ ∈ 𝐴 ((clsβ€˜π‘…)β€˜π‘†)) β†’ 𝑓 ∈ ((clsβ€˜π½)β€˜Xπ‘˜ ∈ 𝐴 𝑆))
15823, 157eqelssd 4004 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 3894   βˆ– cdif 3946   ∩ cin 3948   βŠ† wss 3949  βˆ…c0 4323  βˆͺ cuni 4909  βˆͺ ciun 4998   ↦ cmpt 5232   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  Xcixp 8891  Fincfn 8939  AC wacn 9933  topGenctg 17383  βˆtcpt 17384  Topctop 22395  TopOnctopon 22412  TopBasesctb 22448  Clsdccld 22520  clsccl 22522
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
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 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-iin 5001  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1o 8466  df-er 8703  df-map 8822  df-ixp 8892  df-en 8940  df-fin 8943  df-fi 9406  df-acn 9937  df-topgen 17389  df-pt 17390  df-top 22396  df-topon 22413  df-bases 22449  df-cld 22523  df-ntr 22524  df-cls 22525
This theorem is referenced by:  ptcls  23120  dfac14  23122
  Copyright terms: Public domain W3C validator