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

Theorem ptrescn 21490
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 1086 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → 𝐵𝐴)
2 ptrescn.2 . . . . . . . . . 10 𝐽 = (∏t𝐹)
32ptuni 21445 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑘𝐴 (𝐹𝑘) = 𝐽)
433adant3 1101 . . . . . . . 8 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐴 (𝐹𝑘) = 𝐽)
5 ptrescn.1 . . . . . . . 8 𝑋 = 𝐽
64, 5syl6eqr 2703 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐴 (𝐹𝑘) = 𝑋)
76eleq2d 2716 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑥X𝑘𝐴 (𝐹𝑘) ↔ 𝑥𝑋))
87biimpar 501 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → 𝑥X𝑘𝐴 (𝐹𝑘))
9 resixp 7985 . . . . 5 ((𝐵𝐴𝑥X𝑘𝐴 (𝐹𝑘)) → (𝑥𝐵) ∈ X𝑘𝐵 (𝐹𝑘))
101, 8, 9syl2anc 694 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → (𝑥𝐵) ∈ X𝑘𝐵 (𝐹𝑘))
11 ixpeq2 7964 . . . . . . 7 (∀𝑘𝐵 ((𝐹𝐵)‘𝑘) = (𝐹𝑘) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = X𝑘𝐵 (𝐹𝑘))
12 fvres 6245 . . . . . . . 8 (𝑘𝐵 → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
1312unieqd 4478 . . . . . . 7 (𝑘𝐵 ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
1411, 13mprg 2955 . . . . . 6 X𝑘𝐵 ((𝐹𝐵)‘𝑘) = X𝑘𝐵 (𝐹𝑘)
15 ssexg 4837 . . . . . . . . 9 ((𝐵𝐴𝐴𝑉) → 𝐵 ∈ V)
1615ancoms 468 . . . . . . . 8 ((𝐴𝑉𝐵𝐴) → 𝐵 ∈ V)
17163adant2 1100 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐵 ∈ V)
18 fssres 6108 . . . . . . . 8 ((𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝐹𝐵):𝐵⟶Top)
19183adant1 1099 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝐹𝐵):𝐵⟶Top)
20 ptrescn.3 . . . . . . . 8 𝐾 = (∏t‘(𝐹𝐵))
2120ptuni 21445 . . . . . . 7 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = 𝐾)
2217, 19, 21syl2anc 694 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = 𝐾)
2314, 22syl5eqr 2699 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐵 (𝐹𝑘) = 𝐾)
2423adantr 480 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → X𝑘𝐵 (𝐹𝑘) = 𝐾)
2510, 24eleqtrd 2732 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → (𝑥𝐵) ∈ 𝐾)
26 eqid 2651 . . 3 (𝑥𝑋 ↦ (𝑥𝐵)) = (𝑥𝑋 ↦ (𝑥𝐵))
2725, 26fmptd 6425 . 2 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑥𝑋 ↦ (𝑥𝐵)):𝑋 𝐾)
28 fimacnv 6387 . . . . . . 7 ((𝑥𝑋 ↦ (𝑥𝐵)):𝑋 𝐾 → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) = 𝑋)
2927, 28syl 17 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) = 𝑋)
30 pttop 21433 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) ∈ Top)
312, 30syl5eqel 2734 . . . . . . . 8 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐽 ∈ Top)
32313adant3 1101 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐽 ∈ Top)
335topopn 20759 . . . . . . 7 (𝐽 ∈ Top → 𝑋𝐽)
3432, 33syl 17 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝑋𝐽)
3529, 34eqeltrd 2730 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) ∈ 𝐽)
36 elsni 4227 . . . . . . 7 (𝑣 ∈ { 𝐾} → 𝑣 = 𝐾)
3736imaeq2d 5501 . . . . . 6 (𝑣 ∈ { 𝐾} → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) = ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾))
3837eleq1d 2715 . . . . 5 (𝑣 ∈ { 𝐾} → (((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) ∈ 𝐽))
3935, 38syl5ibrcom 237 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑣 ∈ { 𝐾} → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
4039ralrimiv 2994 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣 ∈ { 𝐾} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
41 imaco 5678 . . . . . . . . 9 (((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘))) “ 𝑢) = ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))
42 cnvco 5340 . . . . . . . . . . 11 ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = ((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘)))
4325adantlr 751 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) ∧ 𝑥𝑋) → (𝑥𝐵) ∈ 𝐾)
44 eqidd 2652 . . . . . . . . . . . . . 14 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑥𝑋 ↦ (𝑥𝐵)) = (𝑥𝑋 ↦ (𝑥𝐵)))
45 eqidd 2652 . . . . . . . . . . . . . 14 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑧 𝐾 ↦ (𝑧𝑘)) = (𝑧 𝐾 ↦ (𝑧𝑘)))
46 fveq1 6228 . . . . . . . . . . . . . 14 (𝑧 = (𝑥𝐵) → (𝑧𝑘) = ((𝑥𝐵)‘𝑘))
4743, 44, 45, 46fmptco 6436 . . . . . . . . . . . . 13 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = (𝑥𝑋 ↦ ((𝑥𝐵)‘𝑘)))
48 fvres 6245 . . . . . . . . . . . . . . 15 (𝑘𝐵 → ((𝑥𝐵)‘𝑘) = (𝑥𝑘))
4948ad2antrl 764 . . . . . . . . . . . . . 14 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝐵)‘𝑘) = (𝑥𝑘))
5049mpteq2dv 4778 . . . . . . . . . . . . 13 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑥𝑋 ↦ ((𝑥𝐵)‘𝑘)) = (𝑥𝑋 ↦ (𝑥𝑘)))
5147, 50eqtrd 2685 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = (𝑥𝑋 ↦ (𝑥𝑘)))
5251cnveqd 5330 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = (𝑥𝑋 ↦ (𝑥𝑘)))
5342, 52syl5eqr 2699 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘))) = (𝑥𝑋 ↦ (𝑥𝑘)))
5453imaeq1d 5500 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘))) “ 𝑢) = ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢))
5541, 54syl5eqr 2699 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) = ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢))
56 simpl1 1084 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝐴𝑉)
57 simpl2 1085 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝐹:𝐴⟶Top)
58 simpl3 1086 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝐵𝐴)
59 simprl 809 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝑘𝐵)
6058, 59sseldd 3637 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝑘𝐴)
615, 2ptpjcn 21462 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝑘𝐴) → (𝑥𝑋 ↦ (𝑥𝑘)) ∈ (𝐽 Cn (𝐹𝑘)))
6256, 57, 60, 61syl3anc 1366 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑥𝑋 ↦ (𝑥𝑘)) ∈ (𝐽 Cn (𝐹𝑘)))
63 simprr 811 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝑢 ∈ (𝐹𝑘))
64 cnima 21117 . . . . . . . . 9 (((𝑥𝑋 ↦ (𝑥𝑘)) ∈ (𝐽 Cn (𝐹𝑘)) ∧ 𝑢 ∈ (𝐹𝑘)) → ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢) ∈ 𝐽)
6562, 63, 64syl2anc 694 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢) ∈ 𝐽)
6655, 65eqeltrd 2730 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ 𝐽)
67 imaeq2 5497 . . . . . . . 8 (𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) = ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
6867eleq1d 2715 . . . . . . 7 (𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → (((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ 𝐽))
6966, 68syl5ibrcom 237 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
7069rexlimdvva 3067 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
7170alrimiv 1895 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣(∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
72 eqid 2651 . . . . . . 7 (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) = (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))
7372rnmpt2 6812 . . . . . 6 ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) = {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)}
7473raleqi 3172 . . . . 5 (∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣 ∈ {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
7512rexeqdv 3175 . . . . . . . 8 (𝑘𝐵 → (∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
76 eqeq1 2655 . . . . . . . . 9 (𝑦 = 𝑣 → (𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ 𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
7776rexbidv 3081 . . . . . . . 8 (𝑦 = 𝑣 → (∃𝑢 ∈ (𝐹𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
7875, 77sylan9bbr 737 . . . . . . 7 ((𝑦 = 𝑣𝑘𝐵) → (∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
7978rexbidva 3078 . . . . . 6 (𝑦 = 𝑣 → (∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
8079ralab 3400 . . . . 5 (∀𝑣 ∈ {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣(∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
8174, 80bitri 264 . . . 4 (∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣(∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
8271, 81sylibr 224 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
83 ralunb 3827 . . 3 (∀𝑣 ∈ ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ (∀𝑣 ∈ { 𝐾} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ∧ ∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
8440, 82, 83sylanbrc 699 . 2 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣 ∈ ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
855toptopon 20770 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
8632, 85sylib 208 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐽 ∈ (TopOn‘𝑋))
87 snex 4938 . . . 4 { 𝐾} ∈ V
88 fvex 6239 . . . . . . . 8 ((𝐹𝐵)‘𝑘) ∈ V
8988abrexex 7183 . . . . . . 7 {𝑦 ∣ ∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V
9089rgenw 2953 . . . . . 6 𝑘𝐵 {𝑦 ∣ ∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V
91 abrexex2g 7186 . . . . . 6 ((𝐵 ∈ V ∧ ∀𝑘𝐵 {𝑦 ∣ ∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V) → {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V)
9217, 90, 91sylancl 695 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V)
9373, 92syl5eqel 2734 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ V)
94 unexg 7001 . . . 4 (({ 𝐾} ∈ V ∧ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ V) → ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))) ∈ V)
9587, 93, 94sylancr 696 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))) ∈ V)
96 eqid 2651 . . . . 5 𝐾 = 𝐾
9720, 96, 72ptval2 21452 . . . 4 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → 𝐾 = (topGen‘(fi‘({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))))))
9817, 19, 97syl2anc 694 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐾 = (topGen‘(fi‘({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))))))
99 pttop 21433 . . . . . 6 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → (∏t‘(𝐹𝐵)) ∈ Top)
10017, 19, 99syl2anc 694 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (∏t‘(𝐹𝐵)) ∈ Top)
10120, 100syl5eqel 2734 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐾 ∈ Top)
10296toptopon 20770 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
103101, 102sylib 208 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐾 ∈ (TopOn‘ 𝐾))
10486, 95, 98, 103subbascn 21106 . 2 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ((𝑥𝑋 ↦ (𝑥𝐵)) ∈ (𝐽 Cn 𝐾) ↔ ((𝑥𝑋 ↦ (𝑥𝐵)):𝑋 𝐾 ∧ ∀𝑣 ∈ ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)))
10527, 84, 104mpbir2and 977 1 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑥𝑋 ↦ (𝑥𝐵)) ∈ (𝐽 Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054  wal 1521   = wceq 1523  wcel 2030  {cab 2637  wral 2941  wrex 2942  Vcvv 3231  cun 3605  wss 3607  {csn 4210   cuni 4468  cmpt 4762  ccnv 5142  ran crn 5144  cres 5145  cima 5146  ccom 5147  wf 5922  cfv 5926  (class class class)co 6690  cmpt2 6692  Xcixp 7950  ficfi 8357  topGenctg 16145  tcpt 16146  Topctop 20746  TopOnctopon 20763   Cn ccn 21076
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-map 7901  df-ixp 7951  df-en 7998  df-dom 7999  df-fin 8001  df-fi 8358  df-topgen 16151  df-pt 16152  df-top 20747  df-topon 20764  df-bases 20798  df-cn 21079
This theorem is referenced by:  ptunhmeo  21659  tmdgsum  21946
  Copyright terms: Public domain W3C validator