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

Theorem ptcnp 23470
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 7077 . . . . . . . . 9 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ Top)
5 toptopon2 22764 . . . . . . . . 9 ((πΉβ€˜π‘˜) ∈ Top ↔ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
64, 5sylib 217 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
7 ptcnp.7 . . . . . . . 8 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·))
8 cnpf2 23098 . . . . . . . 8 ((𝐽 ∈ (TopOnβ€˜π‘‹) ∧ (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)) ∧ (π‘₯ ∈ 𝑋 ↦ 𝐴) ∈ ((𝐽 CnP (πΉβ€˜π‘˜))β€˜π·)) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
92, 6, 7, 8syl3anc 1368 . . . . . . 7 ((πœ‘ ∧ π‘˜ ∈ 𝐼) β†’ (π‘₯ ∈ 𝑋 ↦ 𝐴):π‘‹βŸΆβˆͺ (πΉβ€˜π‘˜))
109fvmptelcdm 7105 . . . . . 6 (((πœ‘ ∧ π‘˜ ∈ 𝐼) ∧ π‘₯ ∈ 𝑋) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
1110an32s 649 . . . . 5 (((πœ‘ ∧ π‘₯ ∈ 𝑋) ∧ π‘˜ ∈ 𝐼) β†’ 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
1211ralrimiva 3138 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜))
13 ptcnp.4 . . . . . 6 (πœ‘ β†’ 𝐼 ∈ 𝑉)
1413adantr 480 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ 𝐼 ∈ 𝑉)
15 mptelixpg 8926 . . . . 5 (𝐼 ∈ 𝑉 β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
1614, 15syl 17 . . . 4 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ ((π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜) ↔ βˆ€π‘˜ ∈ 𝐼 𝐴 ∈ βˆͺ (πΉβ€˜π‘˜)))
1712, 16mpbird 257 . . 3 ((πœ‘ ∧ π‘₯ ∈ 𝑋) β†’ (π‘˜ ∈ 𝐼 ↦ 𝐴) ∈ Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜))
1817fmpttd 7107 . 2 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)):π‘‹βŸΆXπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜))
19 df-3an 1086 . . . . . . . 8 ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)))
20 ptcnp.2 . . . . . . . . . . . . 13 𝐾 = (∏tβ€˜πΉ)
21 ptcnp.6 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 ∈ 𝑋)
22 nfv 1909 . . . . . . . . . . . . . 14 β„²π‘˜(𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))
23 nfv 1909 . . . . . . . . . . . . . . 15 β„²π‘˜(𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))
24 nfcv 2895 . . . . . . . . . . . . . . . . . 18 β„²π‘˜π‘‹
25 nfmpt1 5247 . . . . . . . . . . . . . . . . . 18 β„²π‘˜(π‘˜ ∈ 𝐼 ↦ 𝐴)
2624, 25nfmpt 5246 . . . . . . . . . . . . . . . . 17 β„²π‘˜(π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))
27 nfcv 2895 . . . . . . . . . . . . . . . . 17 β„²π‘˜π·
2826, 27nffv 6892 . . . . . . . . . . . . . . . 16 β„²π‘˜((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·)
2928nfel1 2911 . . . . . . . . . . . . . . 15 β„²π‘˜((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)
3023, 29nfan 1894 . . . . . . . . . . . . . 14 β„²π‘˜((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))
3122, 30nfan 1894 . . . . . . . . . . . . 13 β„²π‘˜((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))
32 simprll 776 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ 𝑔 Fn 𝐼)
33 simprlr 777 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))
34 fveq2 6882 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ (π‘”β€˜π‘›) = (π‘”β€˜π‘˜))
35 fveq2 6882 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘˜))
3634, 35eleq12d 2819 . . . . . . . . . . . . . . 15 (𝑛 = π‘˜ β†’ ((π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ↔ (π‘”β€˜π‘˜) ∈ (πΉβ€˜π‘˜)))
3736rspccva 3603 . . . . . . . . . . . . . 14 ((βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ π‘˜ ∈ 𝐼) β†’ (π‘”β€˜π‘˜) ∈ (πΉβ€˜π‘˜))
3833, 37sylan 579 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) ∧ π‘˜ ∈ 𝐼) β†’ (π‘”β€˜π‘˜) ∈ (πΉβ€˜π‘˜))
39 simprrl 778 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ (𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)))
4039simpld 494 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ 𝑀 ∈ Fin)
4139simprd 495 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))
4235unieqd 4913 . . . . . . . . . . . . . . . 16 (𝑛 = π‘˜ β†’ βˆͺ (πΉβ€˜π‘›) = βˆͺ (πΉβ€˜π‘˜))
4334, 42eqeq12d 2740 . . . . . . . . . . . . . . 15 (𝑛 = π‘˜ β†’ ((π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›) ↔ (π‘”β€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜)))
4443rspccva 3603 . . . . . . . . . . . . . 14 ((βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›) ∧ π‘˜ ∈ (𝐼 βˆ– 𝑀)) β†’ (π‘”β€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜))
4541, 44sylan 579 . . . . . . . . . . . . 13 (((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) ∧ π‘˜ ∈ (𝐼 βˆ– 𝑀)) β†’ (π‘”β€˜π‘˜) = βˆͺ (πΉβ€˜π‘˜))
46 simprrr 779 . . . . . . . . . . . . . 14 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))
4734cbvixpv 8906 . . . . . . . . . . . . . 14 X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)
4846, 47eleqtrdi 2835 . . . . . . . . . . . . 13 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))
4920, 1, 13, 3, 21, 7, 31, 32, 38, 40, 45, 48ptcnplem 23469 . . . . . . . . . . . 12 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
5049anassrs 467 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))) ∧ ((𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
5150expr 456 . . . . . . . . . 10 (((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))) ∧ (𝑀 ∈ Fin ∧ βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
5251rexlimdvaa 3148 . . . . . . . . 9 ((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))) β†’ (βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
5352impr 454 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
5419, 53sylan2b 593 . . . . . . 7 ((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
55 eleq2 2814 . . . . . . . 8 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))
5647eqeq2i 2737 . . . . . . . . . . . 12 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) ↔ 𝑓 = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))
5756biimpi 215 . . . . . . . . . . 11 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ 𝑓 = Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))
5857sseq2d 4007 . . . . . . . . . 10 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓 ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))
5958anbi2d 628 . . . . . . . . 9 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ ((𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓) ↔ (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
6059rexbidv 3170 . . . . . . . 8 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓) ↔ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜))))
6155, 60imbi12d 344 . . . . . . 7 (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ ((((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)) ↔ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† Xπ‘˜ ∈ 𝐼 (π‘”β€˜π‘˜)))))
6254, 61syl5ibrcom 246 . . . . . 6 ((πœ‘ ∧ (𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›))) β†’ (𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
6362expimpd 453 . . . . 5 (πœ‘ β†’ (((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
6463exlimdv 1928 . . . 4 (πœ‘ β†’ (βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
6564alrimiv 1922 . . 3 (πœ‘ β†’ βˆ€π‘“(βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
66 eqeq1 2728 . . . . . 6 (π‘Ž = 𝑓 β†’ (π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›) ↔ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)))
6766anbi2d 628 . . . . 5 (π‘Ž = 𝑓 β†’ (((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) ↔ ((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))))
6867exbidv 1916 . . . 4 (π‘Ž = 𝑓 β†’ (βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) ↔ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))))
6968ralab 3680 . . 3 (βˆ€π‘“ ∈ {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)) ↔ βˆ€π‘“(βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ 𝑓 = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›)) β†’ (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓))))
7065, 69sylibr 233 . 2 (πœ‘ β†’ βˆ€π‘“ ∈ {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)))
713ffnd 6709 . . . . 5 (πœ‘ β†’ 𝐹 Fn 𝐼)
72 eqid 2724 . . . . . 6 {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} = {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}
7372ptval 23418 . . . . 5 ((𝐼 ∈ 𝑉 ∧ 𝐹 Fn 𝐼) β†’ (∏tβ€˜πΉ) = (topGenβ€˜{π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}))
7413, 71, 73syl2anc 583 . . . 4 (πœ‘ β†’ (∏tβ€˜πΉ) = (topGenβ€˜{π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}))
7520, 74eqtrid 2776 . . 3 (πœ‘ β†’ 𝐾 = (topGenβ€˜{π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))}))
763feqmptd 6951 . . . . . 6 (πœ‘ β†’ 𝐹 = (π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜)))
7776fveq2d 6886 . . . . 5 (πœ‘ β†’ (∏tβ€˜πΉ) = (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))))
7820, 77eqtrid 2776 . . . 4 (πœ‘ β†’ 𝐾 = (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))))
796ralrimiva 3138 . . . . 5 (πœ‘ β†’ βˆ€π‘˜ ∈ 𝐼 (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜)))
80 eqid 2724 . . . . . 6 (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))) = (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜)))
8180pttopon 23444 . . . . 5 ((𝐼 ∈ 𝑉 ∧ βˆ€π‘˜ ∈ 𝐼 (πΉβ€˜π‘˜) ∈ (TopOnβ€˜βˆͺ (πΉβ€˜π‘˜))) β†’ (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))) ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜)))
8213, 79, 81syl2anc 583 . . . 4 (πœ‘ β†’ (∏tβ€˜(π‘˜ ∈ 𝐼 ↦ (πΉβ€˜π‘˜))) ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜)))
8378, 82eqeltrd 2825 . . 3 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜Xπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜)))
841, 75, 83, 21tgcnp 23101 . 2 (πœ‘ β†’ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)β€˜π·) ↔ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)):π‘‹βŸΆXπ‘˜ ∈ 𝐼 βˆͺ (πΉβ€˜π‘˜) ∧ βˆ€π‘“ ∈ {π‘Ž ∣ βˆƒπ‘”((𝑔 Fn 𝐼 ∧ βˆ€π‘› ∈ 𝐼 (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ∧ βˆƒπ‘€ ∈ Fin βˆ€π‘› ∈ (𝐼 βˆ– 𝑀)(π‘”β€˜π‘›) = βˆͺ (πΉβ€˜π‘›)) ∧ π‘Ž = X𝑛 ∈ 𝐼 (π‘”β€˜π‘›))} (((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴))β€˜π·) ∈ 𝑓 β†’ βˆƒπ‘§ ∈ 𝐽 (𝐷 ∈ 𝑧 ∧ ((π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) β€œ 𝑧) βŠ† 𝑓)))))
8518, 70, 84mpbir2and 710 1 (πœ‘ β†’ (π‘₯ ∈ 𝑋 ↦ (π‘˜ ∈ 𝐼 ↦ 𝐴)) ∈ ((𝐽 CnP 𝐾)β€˜π·))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1084  βˆ€wal 1531   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098  {cab 2701  βˆ€wral 3053  βˆƒwrex 3062   βˆ– cdif 3938   βŠ† wss 3941  βˆͺ cuni 4900   ↦ cmpt 5222   β€œ cima 5670   Fn wfn 6529  βŸΆwf 6530  β€˜cfv 6534  (class class class)co 7402  Xcixp 8888  Fincfn 8936  topGenctg 17388  βˆtcpt 17389  Topctop 22739  TopOnctopon 22756   CnP ccnp 23073
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-int 4942  df-iun 4990  df-iin 4991  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-1st 7969  df-2nd 7970  df-1o 8462  df-er 8700  df-map 8819  df-ixp 8889  df-en 8937  df-dom 8938  df-fin 8940  df-fi 9403  df-topgen 17394  df-pt 17395  df-top 22740  df-topon 22757  df-bases 22793  df-cnp 23076
This theorem is referenced by:  ptcn  23475
  Copyright terms: Public domain W3C validator