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

Theorem ptrescn 21355
 Description: Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015.)
Hypotheses
Ref Expression
ptrescn.1 𝑋 = 𝐽
ptrescn.2 𝐽 = (∏t𝐹)
ptrescn.3 𝐾 = (∏t‘(𝐹𝐵))
Assertion
Ref Expression
ptrescn ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑥𝑋 ↦ (𝑥𝐵)) ∈ (𝐽 Cn 𝐾))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝑥,𝐾   𝑥,𝑉   𝑥,𝑋
Allowed substitution hint:   𝐽(𝑥)

Proof of Theorem ptrescn
Dummy variables 𝑢 𝑘 𝑣 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl3 1064 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → 𝐵𝐴)
2 ptrescn.2 . . . . . . . . . 10 𝐽 = (∏t𝐹)
32ptuni 21310 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑘𝐴 (𝐹𝑘) = 𝐽)
433adant3 1079 . . . . . . . 8 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐴 (𝐹𝑘) = 𝐽)
5 ptrescn.1 . . . . . . . 8 𝑋 = 𝐽
64, 5syl6eqr 2673 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐴 (𝐹𝑘) = 𝑋)
76eleq2d 2684 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑥X𝑘𝐴 (𝐹𝑘) ↔ 𝑥𝑋))
87biimpar 502 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → 𝑥X𝑘𝐴 (𝐹𝑘))
9 resixp 7890 . . . . 5 ((𝐵𝐴𝑥X𝑘𝐴 (𝐹𝑘)) → (𝑥𝐵) ∈ X𝑘𝐵 (𝐹𝑘))
101, 8, 9syl2anc 692 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → (𝑥𝐵) ∈ X𝑘𝐵 (𝐹𝑘))
11 ixpeq2 7869 . . . . . . 7 (∀𝑘𝐵 ((𝐹𝐵)‘𝑘) = (𝐹𝑘) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = X𝑘𝐵 (𝐹𝑘))
12 fvres 6166 . . . . . . . 8 (𝑘𝐵 → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
1312unieqd 4414 . . . . . . 7 (𝑘𝐵 ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
1411, 13mprg 2921 . . . . . 6 X𝑘𝐵 ((𝐹𝐵)‘𝑘) = X𝑘𝐵 (𝐹𝑘)
15 ssexg 4766 . . . . . . . . 9 ((𝐵𝐴𝐴𝑉) → 𝐵 ∈ V)
1615ancoms 469 . . . . . . . 8 ((𝐴𝑉𝐵𝐴) → 𝐵 ∈ V)
17163adant2 1078 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐵 ∈ V)
18 fssres 6029 . . . . . . . 8 ((𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝐹𝐵):𝐵⟶Top)
19183adant1 1077 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝐹𝐵):𝐵⟶Top)
20 ptrescn.3 . . . . . . . 8 𝐾 = (∏t‘(𝐹𝐵))
2120ptuni 21310 . . . . . . 7 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = 𝐾)
2217, 19, 21syl2anc 692 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = 𝐾)
2314, 22syl5eqr 2669 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐵 (𝐹𝑘) = 𝐾)
2423adantr 481 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → X𝑘𝐵 (𝐹𝑘) = 𝐾)
2510, 24eleqtrd 2700 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → (𝑥𝐵) ∈ 𝐾)
26 eqid 2621 . . 3 (𝑥𝑋 ↦ (𝑥𝐵)) = (𝑥𝑋 ↦ (𝑥𝐵))
2725, 26fmptd 6343 . 2 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑥𝑋 ↦ (𝑥𝐵)):𝑋 𝐾)
28 fimacnv 6305 . . . . . . 7 ((𝑥𝑋 ↦ (𝑥𝐵)):𝑋 𝐾 → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) = 𝑋)
2927, 28syl 17 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) = 𝑋)
30 pttop 21298 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) ∈ Top)
312, 30syl5eqel 2702 . . . . . . . 8 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐽 ∈ Top)
32313adant3 1079 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐽 ∈ Top)
335topopn 20633 . . . . . . 7 (𝐽 ∈ Top → 𝑋𝐽)
3432, 33syl 17 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝑋𝐽)
3529, 34eqeltrd 2698 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) ∈ 𝐽)
36 elsni 4167 . . . . . . 7 (𝑣 ∈ { 𝐾} → 𝑣 = 𝐾)
3736imaeq2d 5427 . . . . . 6 (𝑣 ∈ { 𝐾} → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) = ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾))
3837eleq1d 2683 . . . . 5 (𝑣 ∈ { 𝐾} → (((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) ∈ 𝐽))
3935, 38syl5ibrcom 237 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑣 ∈ { 𝐾} → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
4039ralrimiv 2959 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣 ∈ { 𝐾} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
41 imaco 5601 . . . . . . . . 9 (((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘))) “ 𝑢) = ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))
42 cnvco 5270 . . . . . . . . . . 11 ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = ((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘)))
4325adantlr 750 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) ∧ 𝑥𝑋) → (𝑥𝐵) ∈ 𝐾)
44 eqidd 2622 . . . . . . . . . . . . . 14 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑥𝑋 ↦ (𝑥𝐵)) = (𝑥𝑋 ↦ (𝑥𝐵)))
45 eqidd 2622 . . . . . . . . . . . . . 14 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑧 𝐾 ↦ (𝑧𝑘)) = (𝑧 𝐾 ↦ (𝑧𝑘)))
46 fveq1 6149 . . . . . . . . . . . . . 14 (𝑧 = (𝑥𝐵) → (𝑧𝑘) = ((𝑥𝐵)‘𝑘))
4743, 44, 45, 46fmptco 6354 . . . . . . . . . . . . 13 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = (𝑥𝑋 ↦ ((𝑥𝐵)‘𝑘)))
48 fvres 6166 . . . . . . . . . . . . . . 15 (𝑘𝐵 → ((𝑥𝐵)‘𝑘) = (𝑥𝑘))
4948ad2antrl 763 . . . . . . . . . . . . . 14 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝐵)‘𝑘) = (𝑥𝑘))
5049mpteq2dv 4707 . . . . . . . . . . . . 13 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑥𝑋 ↦ ((𝑥𝐵)‘𝑘)) = (𝑥𝑋 ↦ (𝑥𝑘)))
5147, 50eqtrd 2655 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = (𝑥𝑋 ↦ (𝑥𝑘)))
5251cnveqd 5260 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = (𝑥𝑋 ↦ (𝑥𝑘)))
5342, 52syl5eqr 2669 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘))) = (𝑥𝑋 ↦ (𝑥𝑘)))
5453imaeq1d 5426 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘))) “ 𝑢) = ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢))
5541, 54syl5eqr 2669 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) = ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢))
56 simpl1 1062 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝐴𝑉)
57 simpl2 1063 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝐹:𝐴⟶Top)
58 simpl3 1064 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝐵𝐴)
59 simprl 793 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝑘𝐵)
6058, 59sseldd 3585 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝑘𝐴)
615, 2ptpjcn 21327 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝑘𝐴) → (𝑥𝑋 ↦ (𝑥𝑘)) ∈ (𝐽 Cn (𝐹𝑘)))
6256, 57, 60, 61syl3anc 1323 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑥𝑋 ↦ (𝑥𝑘)) ∈ (𝐽 Cn (𝐹𝑘)))
63 simprr 795 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝑢 ∈ (𝐹𝑘))
64 cnima 20982 . . . . . . . . 9 (((𝑥𝑋 ↦ (𝑥𝑘)) ∈ (𝐽 Cn (𝐹𝑘)) ∧ 𝑢 ∈ (𝐹𝑘)) → ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢) ∈ 𝐽)
6562, 63, 64syl2anc 692 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢) ∈ 𝐽)
6655, 65eqeltrd 2698 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ 𝐽)
67 imaeq2 5423 . . . . . . . 8 (𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) = ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
6867eleq1d 2683 . . . . . . 7 (𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → (((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ 𝐽))
6966, 68syl5ibrcom 237 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
7069rexlimdvva 3031 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
7170alrimiv 1852 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣(∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
72 eqid 2621 . . . . . . 7 (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) = (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))
7372rnmpt2 6726 . . . . . 6 ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) = {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)}
7473raleqi 3131 . . . . 5 (∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣 ∈ {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
7512rexeqdv 3134 . . . . . . . 8 (𝑘𝐵 → (∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
76 eqeq1 2625 . . . . . . . . 9 (𝑦 = 𝑣 → (𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ 𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
7776rexbidv 3045 . . . . . . . 8 (𝑦 = 𝑣 → (∃𝑢 ∈ (𝐹𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
7875, 77sylan9bbr 736 . . . . . . 7 ((𝑦 = 𝑣𝑘𝐵) → (∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
7978rexbidva 3042 . . . . . 6 (𝑦 = 𝑣 → (∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
8079ralab 3350 . . . . 5 (∀𝑣 ∈ {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣(∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
8174, 80bitri 264 . . . 4 (∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣(∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
8271, 81sylibr 224 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
83 ralunb 3774 . . 3 (∀𝑣 ∈ ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ (∀𝑣 ∈ { 𝐾} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ∧ ∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
8440, 82, 83sylanbrc 697 . 2 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣 ∈ ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
855toptopon 20647 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
8632, 85sylib 208 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐽 ∈ (TopOn‘𝑋))
87 snex 4871 . . . 4 { 𝐾} ∈ V
88 fvex 6160 . . . . . . . 8 ((𝐹𝐵)‘𝑘) ∈ V
8988abrexex 7090 . . . . . . 7 {𝑦 ∣ ∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V
9089rgenw 2919 . . . . . 6 𝑘𝐵 {𝑦 ∣ ∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V
91 abrexex2g 7093 . . . . . 6 ((𝐵 ∈ V ∧ ∀𝑘𝐵 {𝑦 ∣ ∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V) → {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V)
9217, 90, 91sylancl 693 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V)
9373, 92syl5eqel 2702 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ V)
94 unexg 6915 . . . 4 (({ 𝐾} ∈ V ∧ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ V) → ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))) ∈ V)
9587, 93, 94sylancr 694 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))) ∈ V)
96 eqid 2621 . . . . 5 𝐾 = 𝐾
9720, 96, 72ptval2 21317 . . . 4 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → 𝐾 = (topGen‘(fi‘({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))))))
9817, 19, 97syl2anc 692 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐾 = (topGen‘(fi‘({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))))))
99 pttop 21298 . . . . . 6 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → (∏t‘(𝐹𝐵)) ∈ Top)
10017, 19, 99syl2anc 692 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (∏t‘(𝐹𝐵)) ∈ Top)
10120, 100syl5eqel 2702 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐾 ∈ Top)
10296toptopon 20647 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
103101, 102sylib 208 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐾 ∈ (TopOn‘ 𝐾))
10486, 95, 98, 103subbascn 20971 . 2 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ((𝑥𝑋 ↦ (𝑥𝐵)) ∈ (𝐽 Cn 𝐾) ↔ ((𝑥𝑋 ↦ (𝑥𝐵)):𝑋 𝐾 ∧ ∀𝑣 ∈ ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)))
10527, 84, 104mpbir2and 956 1 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑥𝑋 ↦ (𝑥𝐵)) ∈ (𝐽 Cn 𝐾))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036  ∀wal 1478   = wceq 1480   ∈ wcel 1987  {cab 2607  ∀wral 2907  ∃wrex 2908  Vcvv 3186   ∪ cun 3554   ⊆ wss 3556  {csn 4150  ∪ cuni 4404   ↦ cmpt 4675  ◡ccnv 5075  ran crn 5077   ↾ cres 5078   “ cima 5079   ∘ ccom 5080  ⟶wf 5845  ‘cfv 5849  (class class class)co 6607   ↦ cmpt2 6609  Xcixp 7855  ficfi 8263  topGenctg 16022  ∏tcpt 16023  Topctop 20620  TopOnctopon 20637   Cn ccn 20941 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-oadd 7512  df-er 7690  df-map 7807  df-ixp 7856  df-en 7903  df-dom 7904  df-fin 7906  df-fi 8264  df-topgen 16028  df-pt 16029  df-top 20621  df-topon 20638  df-bases 20664  df-cn 20944 This theorem is referenced by:  ptunhmeo  21524  tmdgsum  21812
 Copyright terms: Public domain W3C validator