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

Theorem ptcnp 23525
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 480 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ 𝐽 ∈ (TopOnβ€˜π‘‹))
3 ptcnp.5 . . . . . . . . . 10 (πœ‘ β†’ 𝐹:𝐼⟢Top)
43ffvelcdmda 7094 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ Top)
5 toptopon2 22819 . . . . . . . . 9 ((πΉβ€˜π‘˜) ∈ Top ↔ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
64, 5sylib 217 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
7 ptcnp.7 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·))
8 cnpf2 23153 . . . . . . . 8 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)) ∧ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
92, 6, 7, 8syl3anc 1369 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
109fvmptelcdm 7123 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
1110an32s 651 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ π‘˜ ∈ 𝐼) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
1211ralrimiva 3143 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
13 ptcnp.4 . . . . . 6 (πœ‘ β†’ 𝐼 ∈ 𝑉)
1413adantr 480 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐼 ∈ 𝑉)
15 mptelixpg 8953 . . . . 5 (𝐼 ∈ 𝑉 β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
1614, 15syl 17 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
1712, 16mpbird 257 . . 3 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜))
1817fmpttd 7125 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)):π‘‹βŸΆXπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜))
19 df-3an 1087 . . . . . . . 8 ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)))
20 ptcnp.2 . . . . . . . . . . . . 13 𝐾 = (∏tβ€˜πΉ)
21 ptcnp.6 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 ∈ 𝑋)
22 nfv 1910 . . . . . . . . . . . . . 14 β„²π‘˜(𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))
23 nfv 1910 . . . . . . . . . . . . . . 15 β„²π‘˜(𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))
24 nfcv 2899 . . . . . . . . . . . . . . . . . 18 β„²π‘˜π‘‹
25 nfmpt1 5256 . . . . . . . . . . . . . . . . . 18 β„²π‘˜(π‘˜ ∈ 𝐼 ↦ 𝐴)
2624, 25nfmpt 5255 . . . . . . . . . . . . . . . . 17 β„²π‘˜(π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))
27 nfcv 2899 . . . . . . . . . . . . . . . . 17 β„²π‘˜π·
2826, 27nffv 6907 . . . . . . . . . . . . . . . 16 β„²π‘˜((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)
2928nfel1 2916 . . . . . . . . . . . . . . 15 β„²π‘˜((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)
3023, 29nfan 1895 . . . . . . . . . . . . . 14 β„²π‘˜((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))
3122, 30nfan 1895 . . . . . . . . . . . . 13 β„²π‘˜((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))
32 simprll 778 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ 𝑔 Fn 𝐼)
33 simprlr 779 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))
34 fveq2 6897 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ (π‘”β€˜π‘›) = (π‘”β€˜π‘˜))
35 fveq2 6897 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘˜))
3634, 35eleq12d 2823 . . . . . . . . . . . . . . 15 (𝑛 = π‘˜ β†’ ((π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ↔ (π‘”β€˜π‘˜) ∈ (πΉβ€˜π‘˜)))
3736rspccva 3608 . . . . . . . . . . . . . 14 ((βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ π‘˜ ∈ 𝐼) β†’ (π‘”β€˜π‘˜) ∈ (πΉβ€˜π‘˜))
3833, 37sylan 579 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) ∧ π‘˜ ∈ 𝐼) β†’ (π‘”β€˜π‘˜) ∈ (πΉβ€˜π‘˜))
39 simprrl 780 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ (𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)))
4039simpld 494 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ 𝑀 ∈ Fin)
4139simprd 495 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))
4235unieqd 4921 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ βˆͺ (πΉβ€˜π‘›) = βˆͺ (πΉβ€˜π‘˜))
4334, 42eqeq12d 2744 . . . . . . . . . . . . . . 15 (𝑛 = π‘˜ β†’ ((π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›) ↔ (π‘”β€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜)))
4443rspccva 3608 . . . . . . . . . . . . . 14 ((βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›) ∧ π‘˜ ∈ (𝐼 βˆ– 𝑀)) β†’ (π‘”β€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜))
4541, 44sylan 579 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) ∧ π‘˜ ∈ (𝐼 βˆ– 𝑀)) β†’ (π‘”β€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜))
46 simprrr 781 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))
4734cbvixpv 8933 . . . . . . . . . . . . . 14 X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)
4846, 47eleqtrdi 2839 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))
4920, 1, 13, 3, 21, 7, 31, 32, 38, 40, 45, 48ptcnplem 23524 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
5049anassrs 467 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
5150expr 456 . . . . . . . . . 10 (((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))) ∧ (𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
5251rexlimdvaa 3153 . . . . . . . . 9 ((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))) β†’ (βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
5352impr 454 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
5419, 53sylan2b 593 . . . . . . 7 ((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
55 eleq2 2818 . . . . . . . 8 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))
5647eqeq2i 2741 . . . . . . . . . . . 12 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) ↔ 𝑓 = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))
5756biimpi 215 . . . . . . . . . . 11 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ 𝑓 = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))
5857sseq2d 4012 . . . . . . . . . 10 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓 ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
5958anbi2d 629 . . . . . . . . 9 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ ((𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓) ↔ (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
6059rexbidv 3175 . . . . . . . 8 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓) ↔ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
6155, 60imbi12d 344 . . . . . . 7 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ ((((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)) ↔ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
6254, 61syl5ibrcom 246 . . . . . 6 ((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
6362expimpd 453 . . . . 5 (πœ‘ β†’ (((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
6463exlimdv 1929 . . . 4 (πœ‘ β†’ (βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
6564alrimiv 1923 . . 3 (πœ‘ β†’ βˆ€π‘“(βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
66 eqeq1 2732 . . . . . 6 (π‘Ž = 𝑓 β†’ (π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) ↔ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))
6766anbi2d 629 . . . . 5 (π‘Ž = 𝑓 β†’ (((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))))
6867exbidv 1917 . . . 4 (π‘Ž = 𝑓 β†’ (βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) ↔ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))))
6968ralab 3686 . . 3 (βˆ€π‘“ ∈ {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)) ↔ βˆ€π‘“(βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
7065, 69sylibr 233 . 2 (πœ‘ β†’ βˆ€π‘“ ∈ {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)))
713ffnd 6723 . . . . 5 (πœ‘ β†’ 𝐹 Fn 𝐼)
72 eqid 2728 . . . . . 6 {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} = {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}
7372ptval 23473 . . . . 5 ((𝐼 ∈ 𝑉 ∧ 𝐹 Fn 𝐼) β†’ (∏tβ€˜πΉ) = (topGenβ€˜{π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}))
7413, 71, 73syl2anc 583 . . . 4 (πœ‘ β†’ (∏tβ€˜πΉ) = (topGenβ€˜{π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}))
7520, 74eqtrid 2780 . . 3 (πœ‘ β†’ 𝐾 = (topGenβ€˜{π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}))
763feqmptd 6967 . . . . . 6 (πœ‘ β†’ 𝐹 = (π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜)))
7776fveq2d 6901 . . . . 5 (πœ‘ β†’ (∏tβ€˜πΉ) = (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))))
7820, 77eqtrid 2780 . . . 4 (πœ‘ β†’ 𝐾 = (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))))
796ralrimiva 3143 . . . . 5 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐼 (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
80 eqid 2728 . . . . . 6 (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))) = (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜)))
8180pttopon 23499 . . . . 5 ((𝐼 ∈ 𝑉 ∧ βˆ€π‘˜ ∈ 𝐼 (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜))) β†’ (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))) ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜)))
8213, 79, 81syl2anc 583 . . . 4 (πœ‘ β†’ (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))) ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜)))
8378, 82eqeltrd 2829 . . 3 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜)))
841, 75, 83, 21tgcnp 23156 . 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 395   ∧ w3a 1085  βˆ€wal 1532   = wceq 1534  βˆƒwex 1774   ∈ wcel 2099  {cab 2705  βˆ€wral 3058  βˆƒwrex 3067   βˆ– cdif 3944   βŠ† wss 3947  βˆͺ cuni 4908   ↦ cmpt 5231   β€œ cima 5681   Fn wfn 6543  βŸΆwf 6544  β€˜cfv 6548  (class class class)co 7420  Xcixp 8915  Fincfn 8963  topGenctg 17418  βˆtcpt 17419  Topctop 22794  TopOnctopon 22811   CnP ccnp 23128
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7871  df-1st 7993  df-2nd 7994  df-1o 8486  df-er 8724  df-map 8846  df-ixp 8916  df-en 8964  df-dom 8965  df-fin 8967  df-fi 9434  df-topgen 17424  df-pt 17425  df-top 22795  df-topon 22812  df-bases 22848  df-cnp 23131
This theorem is referenced by:  ptcn  23530
  Copyright terms: Public domain W3C validator