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

Theorem ptcnp 21235
 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 . . . . . . . . . 10 (𝜑𝐽 ∈ (TopOn‘𝑋))
21adantr 480 . . . . . . . . 9 ((𝜑𝑘𝐼) → 𝐽 ∈ (TopOn‘𝑋))
3 ptcnp.5 . . . . . . . . . . 11 (𝜑𝐹:𝐼⟶Top)
43ffvelrnda 6267 . . . . . . . . . 10 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ Top)
5 eqid 2610 . . . . . . . . . . 11 (𝐹𝑘) = (𝐹𝑘)
65toptopon 20548 . . . . . . . . . 10 ((𝐹𝑘) ∈ Top ↔ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
74, 6sylib 207 . . . . . . . . 9 ((𝜑𝑘𝐼) → (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
8 ptcnp.7 . . . . . . . . 9 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷))
9 cnpf2 20864 . . . . . . . . 9 ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)) ∧ (𝑥𝑋𝐴) ∈ ((𝐽 CnP (𝐹𝑘))‘𝐷)) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
102, 7, 8, 9syl3anc 1318 . . . . . . . 8 ((𝜑𝑘𝐼) → (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
11 eqid 2610 . . . . . . . . 9 (𝑥𝑋𝐴) = (𝑥𝑋𝐴)
1211fmpt 6289 . . . . . . . 8 (∀𝑥𝑋 𝐴 (𝐹𝑘) ↔ (𝑥𝑋𝐴):𝑋 (𝐹𝑘))
1310, 12sylibr 223 . . . . . . 7 ((𝜑𝑘𝐼) → ∀𝑥𝑋 𝐴 (𝐹𝑘))
1413r19.21bi 2916 . . . . . 6 (((𝜑𝑘𝐼) ∧ 𝑥𝑋) → 𝐴 (𝐹𝑘))
1514an32s 842 . . . . 5 (((𝜑𝑥𝑋) ∧ 𝑘𝐼) → 𝐴 (𝐹𝑘))
1615ralrimiva 2949 . . . 4 ((𝜑𝑥𝑋) → ∀𝑘𝐼 𝐴 (𝐹𝑘))
17 ptcnp.4 . . . . . 6 (𝜑𝐼𝑉)
1817adantr 480 . . . . 5 ((𝜑𝑥𝑋) → 𝐼𝑉)
19 mptelixpg 7831 . . . . 5 (𝐼𝑉 → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐹𝑘) ↔ ∀𝑘𝐼 𝐴 (𝐹𝑘)))
2018, 19syl 17 . . . 4 ((𝜑𝑥𝑋) → ((𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐹𝑘) ↔ ∀𝑘𝐼 𝐴 (𝐹𝑘)))
2116, 20mpbird 246 . . 3 ((𝜑𝑥𝑋) → (𝑘𝐼𝐴) ∈ X𝑘𝐼 (𝐹𝑘))
22 eqid 2610 . . 3 (𝑥𝑋 ↦ (𝑘𝐼𝐴)) = (𝑥𝑋 ↦ (𝑘𝐼𝐴))
2321, 22fmptd 6292 . 2 (𝜑 → (𝑥𝑋 ↦ (𝑘𝐼𝐴)):𝑋X𝑘𝐼 (𝐹𝑘))
24 df-3an 1033 . . . . . . . 8 ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)))
25 ptcnp.2 . . . . . . . . . . . . 13 𝐾 = (∏t𝐹)
26 ptcnp.6 . . . . . . . . . . . . 13 (𝜑𝐷𝑋)
27 nfv 1830 . . . . . . . . . . . . . 14 𝑘(𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛))
28 nfv 1830 . . . . . . . . . . . . . . 15 𝑘(𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛))
29 nfcv 2751 . . . . . . . . . . . . . . . . . 18 𝑘𝑋
30 nfmpt1 4675 . . . . . . . . . . . . . . . . . 18 𝑘(𝑘𝐼𝐴)
3129, 30nfmpt 4674 . . . . . . . . . . . . . . . . 17 𝑘(𝑥𝑋 ↦ (𝑘𝐼𝐴))
32 nfcv 2751 . . . . . . . . . . . . . . . . 17 𝑘𝐷
3331, 32nffv 6110 . . . . . . . . . . . . . . . 16 𝑘((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷)
3433nfel1 2765 . . . . . . . . . . . . . . 15 𝑘((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)
3528, 34nfan 1816 . . . . . . . . . . . . . 14 𝑘((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛))
3627, 35nfan 1816 . . . . . . . . . . . . 13 𝑘((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))
37 simprll 798 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))) → 𝑔 Fn 𝐼)
38 simprlr 799 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))) → ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛))
39 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → (𝑔𝑛) = (𝑔𝑘))
40 fveq2 6103 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
4139, 40eleq12d 2682 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → ((𝑔𝑛) ∈ (𝐹𝑛) ↔ (𝑔𝑘) ∈ (𝐹𝑘)))
4241rspccva 3281 . . . . . . . . . . . . . 14 ((∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ 𝑘𝐼) → (𝑔𝑘) ∈ (𝐹𝑘))
4338, 42sylan 487 . . . . . . . . . . . . 13 (((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))) ∧ 𝑘𝐼) → (𝑔𝑘) ∈ (𝐹𝑘))
44 simprrl 800 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))) → (𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)))
4544simpld 474 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))) → 𝑤 ∈ Fin)
4644simprd 478 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))) → ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛))
4740unieqd 4382 . . . . . . . . . . . . . . . 16 (𝑛 = 𝑘 (𝐹𝑛) = (𝐹𝑘))
4839, 47eqeq12d 2625 . . . . . . . . . . . . . . 15 (𝑛 = 𝑘 → ((𝑔𝑛) = (𝐹𝑛) ↔ (𝑔𝑘) = (𝐹𝑘)))
4948rspccva 3281 . . . . . . . . . . . . . 14 ((∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛) ∧ 𝑘 ∈ (𝐼𝑤)) → (𝑔𝑘) = (𝐹𝑘))
5046, 49sylan 487 . . . . . . . . . . . . 13 (((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))) ∧ 𝑘 ∈ (𝐼𝑤)) → (𝑔𝑘) = (𝐹𝑘))
51 simprrr 801 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛))
5239cbvixpv 7812 . . . . . . . . . . . . . 14 X𝑛𝐼 (𝑔𝑛) = X𝑘𝐼 (𝑔𝑘)
5351, 52syl6eleq 2698 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))) → ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑘𝐼 (𝑔𝑘))
5425, 1, 17, 3, 26, 8, 36, 37, 43, 45, 50, 53ptcnplem 21234 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝑔𝑘)))
5554anassrs 678 . . . . . . . . . . 11 (((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛))) ∧ ((𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛))) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝑔𝑘)))
5655expr 641 . . . . . . . . . 10 (((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛))) ∧ (𝑤 ∈ Fin ∧ ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝑔𝑘))))
5756rexlimdvaa 3014 . . . . . . . . 9 ((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛))) → (∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝑔𝑘)))))
5857impr 647 . . . . . . . 8 ((𝜑 ∧ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛)) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝑔𝑘))))
5924, 58sylan2b 491 . . . . . . 7 ((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛))) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝑔𝑘))))
60 eleq2 2677 . . . . . . . 8 (𝑓 = X𝑛𝐼 (𝑔𝑛) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ 𝑓 ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛)))
6152eqeq2i 2622 . . . . . . . . . . . 12 (𝑓 = X𝑛𝐼 (𝑔𝑛) ↔ 𝑓 = X𝑘𝐼 (𝑔𝑘))
6261biimpi 205 . . . . . . . . . . 11 (𝑓 = X𝑛𝐼 (𝑔𝑛) → 𝑓 = X𝑘𝐼 (𝑔𝑘))
6362sseq2d 3596 . . . . . . . . . 10 (𝑓 = X𝑛𝐼 (𝑔𝑛) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓 ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝑔𝑘)))
6463anbi2d 736 . . . . . . . . 9 (𝑓 = X𝑛𝐼 (𝑔𝑛) → ((𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓) ↔ (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝑔𝑘))))
6564rexbidv 3034 . . . . . . . 8 (𝑓 = X𝑛𝐼 (𝑔𝑛) → (∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓) ↔ ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝑔𝑘))))
6660, 65imbi12d 333 . . . . . . 7 (𝑓 = X𝑛𝐼 (𝑔𝑛) → ((((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓)) ↔ (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ X𝑛𝐼 (𝑔𝑛) → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ X𝑘𝐼 (𝑔𝑘)))))
6759, 66syl5ibrcom 236 . . . . . 6 ((𝜑 ∧ (𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛))) → (𝑓 = X𝑛𝐼 (𝑔𝑛) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓))))
6867expimpd 627 . . . . 5 (𝜑 → (((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑓 = X𝑛𝐼 (𝑔𝑛)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓))))
6968exlimdv 1848 . . . 4 (𝜑 → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑓 = X𝑛𝐼 (𝑔𝑛)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓))))
7069alrimiv 1842 . . 3 (𝜑 → ∀𝑓(∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑓 = X𝑛𝐼 (𝑔𝑛)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓))))
71 eqeq1 2614 . . . . . 6 (𝑎 = 𝑓 → (𝑎 = X𝑛𝐼 (𝑔𝑛) ↔ 𝑓 = X𝑛𝐼 (𝑔𝑛)))
7271anbi2d 736 . . . . 5 (𝑎 = 𝑓 → (((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑎 = X𝑛𝐼 (𝑔𝑛)) ↔ ((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑓 = X𝑛𝐼 (𝑔𝑛))))
7372exbidv 1837 . . . 4 (𝑎 = 𝑓 → (∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑎 = X𝑛𝐼 (𝑔𝑛)) ↔ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑓 = X𝑛𝐼 (𝑔𝑛))))
7473ralab 3334 . . 3 (∀𝑓 ∈ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑎 = X𝑛𝐼 (𝑔𝑛))} (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓)) ↔ ∀𝑓(∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑓 = X𝑛𝐼 (𝑔𝑛)) → (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓))))
7570, 74sylibr 223 . 2 (𝜑 → ∀𝑓 ∈ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑎 = X𝑛𝐼 (𝑔𝑛))} (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓)))
76 ffn 5958 . . . . . 6 (𝐹:𝐼⟶Top → 𝐹 Fn 𝐼)
773, 76syl 17 . . . . 5 (𝜑𝐹 Fn 𝐼)
78 eqid 2610 . . . . . 6 {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑎 = X𝑛𝐼 (𝑔𝑛))} = {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑎 = X𝑛𝐼 (𝑔𝑛))}
7978ptval 21183 . . . . 5 ((𝐼𝑉𝐹 Fn 𝐼) → (∏t𝐹) = (topGen‘{𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑎 = X𝑛𝐼 (𝑔𝑛))}))
8017, 77, 79syl2anc 691 . . . 4 (𝜑 → (∏t𝐹) = (topGen‘{𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑎 = X𝑛𝐼 (𝑔𝑛))}))
8125, 80syl5eq 2656 . . 3 (𝜑𝐾 = (topGen‘{𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑎 = X𝑛𝐼 (𝑔𝑛))}))
823feqmptd 6159 . . . . . 6 (𝜑𝐹 = (𝑘𝐼 ↦ (𝐹𝑘)))
8382fveq2d 6107 . . . . 5 (𝜑 → (∏t𝐹) = (∏t‘(𝑘𝐼 ↦ (𝐹𝑘))))
8425, 83syl5eq 2656 . . . 4 (𝜑𝐾 = (∏t‘(𝑘𝐼 ↦ (𝐹𝑘))))
857ralrimiva 2949 . . . . 5 (𝜑 → ∀𝑘𝐼 (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘)))
86 eqid 2610 . . . . . 6 (∏t‘(𝑘𝐼 ↦ (𝐹𝑘))) = (∏t‘(𝑘𝐼 ↦ (𝐹𝑘)))
8786pttopon 21209 . . . . 5 ((𝐼𝑉 ∧ ∀𝑘𝐼 (𝐹𝑘) ∈ (TopOn‘ (𝐹𝑘))) → (∏t‘(𝑘𝐼 ↦ (𝐹𝑘))) ∈ (TopOn‘X𝑘𝐼 (𝐹𝑘)))
8817, 85, 87syl2anc 691 . . . 4 (𝜑 → (∏t‘(𝑘𝐼 ↦ (𝐹𝑘))) ∈ (TopOn‘X𝑘𝐼 (𝐹𝑘)))
8984, 88eqeltrd 2688 . . 3 (𝜑𝐾 ∈ (TopOn‘X𝑘𝐼 (𝐹𝑘)))
901, 81, 89, 26tgcnp 20867 . 2 (𝜑 → ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝐷) ↔ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)):𝑋X𝑘𝐼 (𝐹𝑘) ∧ ∀𝑓 ∈ {𝑎 ∣ ∃𝑔((𝑔 Fn 𝐼 ∧ ∀𝑛𝐼 (𝑔𝑛) ∈ (𝐹𝑛) ∧ ∃𝑤 ∈ Fin ∀𝑛 ∈ (𝐼𝑤)(𝑔𝑛) = (𝐹𝑛)) ∧ 𝑎 = X𝑛𝐼 (𝑔𝑛))} (((𝑥𝑋 ↦ (𝑘𝐼𝐴))‘𝐷) ∈ 𝑓 → ∃𝑧𝐽 (𝐷𝑧 ∧ ((𝑥𝑋 ↦ (𝑘𝐼𝐴)) “ 𝑧) ⊆ 𝑓)))))
9123, 75, 90mpbir2and 959 1 (𝜑 → (𝑥𝑋 ↦ (𝑘𝐼𝐴)) ∈ ((𝐽 CnP 𝐾)‘𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897   ∖ cdif 3537   ⊆ wss 3540  ∪ cuni 4372   ↦ cmpt 4643   “ cima 5041   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  Xcixp 7794  Fincfn 7841  topGenctg 15921  ∏tcpt 15922  Topctop 20517  TopOnctopon 20518   CnP ccnp 20839 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-fin 7845  df-fi 8200  df-topgen 15927  df-pt 15928  df-top 20521  df-bases 20522  df-topon 20523  df-cnp 20842 This theorem is referenced by:  ptcn  21240
 Copyright terms: Public domain W3C validator