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

Theorem ptcnp 22989
Description: If every projection of a function is continuous at 𝐷, then the function itself is continuous at 𝐷 into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
ptcnp.2 𝐾 = (∏tβ€˜πΉ)
ptcnp.3 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
ptcnp.4 (πœ‘ β†’ 𝐼 ∈ 𝑉)
ptcnp.5 (πœ‘ β†’ 𝐹:𝐼⟢Top)
ptcnp.6 (πœ‘ β†’ 𝐷 ∈ 𝑋)
ptcnp.7 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·))
Assertion
Ref Expression
ptcnp (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)β€˜π·))
Distinct variable groups:   π‘₯,π‘˜,𝐷   π‘˜,𝐼,π‘₯   π‘˜,𝐽   πœ‘,π‘˜,π‘₯   π‘˜,𝐹,π‘₯   π‘˜,𝑉,π‘₯   π‘˜,𝑋,π‘₯
Allowed substitution hints:   𝐴(π‘₯,π‘˜)   𝐽(π‘₯)   𝐾(π‘₯,π‘˜)

Proof of Theorem ptcnp
Dummy variables 𝑓 𝑔 𝑀 𝑧 π‘Ž 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptcnp.3 . . . . . . . . 9 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
21adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
3 ptcnp.5 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:𝐼⟢Top)
43ffvelcdmda 7036 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ Top)
5 toptopon2 22283 . . . . . . . . 9 ((πΉβ€˜π‘˜) ∈ Top ↔ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
64, 5sylib 217 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
7 ptcnp.7 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·))
8 cnpf2 22617 . . . . . . . 8 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)) ∧ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
92, 6, 7, 8syl3anc 1372 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
109fvmptelcdm 7062 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
1110an32s 651 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ π‘˜ ∈ 𝐼) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
1211ralrimiva 3140 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
13 ptcnp.4 . . . . . 6 (πœ‘ β†’ 𝐼 ∈ 𝑉)
1413adantr 482 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐼 ∈ 𝑉)
15 mptelixpg 8876 . . . . 5 (𝐼 ∈ 𝑉 β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
1614, 15syl 17 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
1712, 16mpbird 257 . . 3 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜))
1817fmpttd 7064 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)):π‘‹βŸΆXπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜))
19 df-3an 1090 . . . . . . . 8 ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)))
20 ptcnp.2 . . . . . . . . . . . . 13 𝐾 = (∏tβ€˜πΉ)
21 ptcnp.6 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 ∈ 𝑋)
22 nfv 1918 . . . . . . . . . . . . . 14 β„²π‘˜(𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))
23 nfv 1918 . . . . . . . . . . . . . . 15 β„²π‘˜(𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))
24 nfcv 2904 . . . . . . . . . . . . . . . . . 18 β„²π‘˜π‘‹
25 nfmpt1 5214 . . . . . . . . . . . . . . . . . 18 β„²π‘˜(π‘˜ ∈ 𝐼 ↦ 𝐴)
2624, 25nfmpt 5213 . . . . . . . . . . . . . . . . 17 β„²π‘˜(π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))
27 nfcv 2904 . . . . . . . . . . . . . . . . 17 β„²π‘˜π·
2826, 27nffv 6853 . . . . . . . . . . . . . . . 16 β„²π‘˜((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)
2928nfel1 2920 . . . . . . . . . . . . . . 15 β„²π‘˜((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)
3023, 29nfan 1903 . . . . . . . . . . . . . 14 β„²π‘˜((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))
3122, 30nfan 1903 . . . . . . . . . . . . 13 β„²π‘˜((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))
32 simprll 778 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ 𝑔 Fn 𝐼)
33 simprlr 779 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))
34 fveq2 6843 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ (π‘”β€˜π‘›) = (π‘”β€˜π‘˜))
35 fveq2 6843 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘˜))
3634, 35eleq12d 2828 . . . . . . . . . . . . . . 15 (𝑛 = π‘˜ β†’ ((π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ↔ (π‘”β€˜π‘˜) ∈ (πΉβ€˜π‘˜)))
3736rspccva 3579 . . . . . . . . . . . . . 14 ((βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ π‘˜ ∈ 𝐼) β†’ (π‘”β€˜π‘˜) ∈ (πΉβ€˜π‘˜))
3833, 37sylan 581 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) ∧ π‘˜ ∈ 𝐼) β†’ (π‘”β€˜π‘˜) ∈ (πΉβ€˜π‘˜))
39 simprrl 780 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ (𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)))
4039simpld 496 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ 𝑀 ∈ Fin)
4139simprd 497 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))
4235unieqd 4880 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ βˆͺ (πΉβ€˜π‘›) = βˆͺ (πΉβ€˜π‘˜))
4334, 42eqeq12d 2749 . . . . . . . . . . . . . . 15 (𝑛 = π‘˜ β†’ ((π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›) ↔ (π‘”β€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜)))
4443rspccva 3579 . . . . . . . . . . . . . 14 ((βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›) ∧ π‘˜ ∈ (𝐼 βˆ– 𝑀)) β†’ (π‘”β€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜))
4541, 44sylan 581 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) ∧ π‘˜ ∈ (𝐼 βˆ– 𝑀)) β†’ (π‘”β€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜))
46 simprrr 781 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))
4734cbvixpv 8856 . . . . . . . . . . . . . 14 X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)
4846, 47eleqtrdi 2844 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))
4920, 1, 13, 3, 21, 7, 31, 32, 38, 40, 45, 48ptcnplem 22988 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
5049anassrs 469 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
5150expr 458 . . . . . . . . . 10 (((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))) ∧ (𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
5251rexlimdvaa 3150 . . . . . . . . 9 ((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))) β†’ (βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
5352impr 456 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
5419, 53sylan2b 595 . . . . . . 7 ((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
55 eleq2 2823 . . . . . . . 8 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))
5647eqeq2i 2746 . . . . . . . . . . . 12 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) ↔ 𝑓 = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))
5756biimpi 215 . . . . . . . . . . 11 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ 𝑓 = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))
5857sseq2d 3977 . . . . . . . . . 10 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓 ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
5958anbi2d 630 . . . . . . . . 9 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ ((𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓) ↔ (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
6059rexbidv 3172 . . . . . . . 8 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓) ↔ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
6155, 60imbi12d 345 . . . . . . 7 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ ((((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)) ↔ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
6254, 61syl5ibrcom 247 . . . . . 6 ((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
6362expimpd 455 . . . . 5 (πœ‘ β†’ (((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
6463exlimdv 1937 . . . 4 (πœ‘ β†’ (βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
6564alrimiv 1931 . . 3 (πœ‘ β†’ βˆ€π‘“(βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
66 eqeq1 2737 . . . . . 6 (π‘Ž = 𝑓 β†’ (π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) ↔ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))
6766anbi2d 630 . . . . 5 (π‘Ž = 𝑓 β†’ (((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))))
6867exbidv 1925 . . . 4 (π‘Ž = 𝑓 β†’ (βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) ↔ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))))
6968ralab 3650 . . 3 (βˆ€π‘“ ∈ {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)) ↔ βˆ€π‘“(βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
7065, 69sylibr 233 . 2 (πœ‘ β†’ βˆ€π‘“ ∈ {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)))
713ffnd 6670 . . . . 5 (πœ‘ β†’ 𝐹 Fn 𝐼)
72 eqid 2733 . . . . . 6 {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} = {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}
7372ptval 22937 . . . . 5 ((𝐼 ∈ 𝑉 ∧ 𝐹 Fn 𝐼) β†’ (∏tβ€˜πΉ) = (topGenβ€˜{π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}))
7413, 71, 73syl2anc 585 . . . 4 (πœ‘ β†’ (∏tβ€˜πΉ) = (topGenβ€˜{π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}))
7520, 74eqtrid 2785 . . 3 (πœ‘ β†’ 𝐾 = (topGenβ€˜{π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}))
763feqmptd 6911 . . . . . 6 (πœ‘ β†’ 𝐹 = (π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜)))
7776fveq2d 6847 . . . . 5 (πœ‘ β†’ (∏tβ€˜πΉ) = (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))))
7820, 77eqtrid 2785 . . . 4 (πœ‘ β†’ 𝐾 = (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))))
796ralrimiva 3140 . . . . 5 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐼 (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
80 eqid 2733 . . . . . 6 (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))) = (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜)))
8180pttopon 22963 . . . . 5 ((𝐼 ∈ 𝑉 ∧ βˆ€π‘˜ ∈ 𝐼 (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜))) β†’ (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))) ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜)))
8213, 79, 81syl2anc 585 . . . 4 (πœ‘ β†’ (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))) ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜)))
8378, 82eqeltrd 2834 . . 3 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜)))
841, 75, 83, 21tgcnp 22620 . 2 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)β€˜π·) ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)):π‘‹βŸΆXπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜) ∧ βˆ€π‘“ ∈ {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)))))
8518, 70, 84mpbir2and 712 1 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)β€˜π·))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088  βˆ€wal 1540   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  {cab 2710  βˆ€wral 3061  βˆƒwrex 3070   βˆ– cdif 3908   βŠ† wss 3911  βˆͺ cuni 4866   ↦ cmpt 5189   β€œ cima 5637   Fn wfn 6492  βŸΆwf 6493  β€˜cfv 6497  (class class class)co 7358  Xcixp 8838  Fincfn 8886  topGenctg 17324  βˆtcpt 17325  Topctop 22258  TopOnctopon 22275   CnP ccnp 22592
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 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
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 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-iin 4958  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-1st 7922  df-2nd 7923  df-1o 8413  df-er 8651  df-map 8770  df-ixp 8839  df-en 8887  df-dom 8888  df-fin 8890  df-fi 9352  df-topgen 17330  df-pt 17331  df-top 22259  df-topon 22276  df-bases 22312  df-cnp 22595
This theorem is referenced by:  ptcn  22994
  Copyright terms: Public domain W3C validator