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

Theorem ptrescn 21935
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 1186 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → 𝐵𝐴)
2 ptrescn.2 . . . . . . . . . 10 𝐽 = (∏t𝐹)
32ptuni 21890 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑘𝐴 (𝐹𝑘) = 𝐽)
433adant3 1125 . . . . . . . 8 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐴 (𝐹𝑘) = 𝐽)
5 ptrescn.1 . . . . . . . 8 𝑋 = 𝐽
64, 5syl6eqr 2851 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐴 (𝐹𝑘) = 𝑋)
76eleq2d 2870 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑥X𝑘𝐴 (𝐹𝑘) ↔ 𝑥𝑋))
87biimpar 478 . . . . 5 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → 𝑥X𝑘𝐴 (𝐹𝑘))
9 resixp 8352 . . . . 5 ((𝐵𝐴𝑥X𝑘𝐴 (𝐹𝑘)) → (𝑥𝐵) ∈ X𝑘𝐵 (𝐹𝑘))
101, 8, 9syl2anc 584 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → (𝑥𝐵) ∈ X𝑘𝐵 (𝐹𝑘))
11 ixpeq2 8331 . . . . . . 7 (∀𝑘𝐵 ((𝐹𝐵)‘𝑘) = (𝐹𝑘) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = X𝑘𝐵 (𝐹𝑘))
12 fvres 6564 . . . . . . . 8 (𝑘𝐵 → ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
1312unieqd 4761 . . . . . . 7 (𝑘𝐵 ((𝐹𝐵)‘𝑘) = (𝐹𝑘))
1411, 13mprg 3121 . . . . . 6 X𝑘𝐵 ((𝐹𝐵)‘𝑘) = X𝑘𝐵 (𝐹𝑘)
15 ssexg 5125 . . . . . . . . 9 ((𝐵𝐴𝐴𝑉) → 𝐵 ∈ V)
1615ancoms 459 . . . . . . . 8 ((𝐴𝑉𝐵𝐴) → 𝐵 ∈ V)
17163adant2 1124 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐵 ∈ V)
18 fssres 6419 . . . . . . . 8 ((𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝐹𝐵):𝐵⟶Top)
19183adant1 1123 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝐹𝐵):𝐵⟶Top)
20 ptrescn.3 . . . . . . . 8 𝐾 = (∏t‘(𝐹𝐵))
2120ptuni 21890 . . . . . . 7 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = 𝐾)
2217, 19, 21syl2anc 584 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐵 ((𝐹𝐵)‘𝑘) = 𝐾)
2314, 22syl5eqr 2847 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → X𝑘𝐵 (𝐹𝑘) = 𝐾)
2423adantr 481 . . . 4 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → X𝑘𝐵 (𝐹𝑘) = 𝐾)
2510, 24eleqtrd 2887 . . 3 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ 𝑥𝑋) → (𝑥𝐵) ∈ 𝐾)
2625fmpttd 6749 . 2 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑥𝑋 ↦ (𝑥𝐵)):𝑋 𝐾)
27 fimacnv 6711 . . . . . . 7 ((𝑥𝑋 ↦ (𝑥𝐵)):𝑋 𝐾 → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) = 𝑋)
2826, 27syl 17 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) = 𝑋)
29 pttop 21878 . . . . . . . . 9 ((𝐴𝑉𝐹:𝐴⟶Top) → (∏t𝐹) ∈ Top)
302, 29syl5eqel 2889 . . . . . . . 8 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐽 ∈ Top)
31303adant3 1125 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐽 ∈ Top)
325topopn 21202 . . . . . . 7 (𝐽 ∈ Top → 𝑋𝐽)
3331, 32syl 17 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝑋𝐽)
3428, 33eqeltrd 2885 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) ∈ 𝐽)
35 elsni 4495 . . . . . . 7 (𝑣 ∈ { 𝐾} → 𝑣 = 𝐾)
3635imaeq2d 5813 . . . . . 6 (𝑣 ∈ { 𝐾} → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) = ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾))
3736eleq1d 2869 . . . . 5 (𝑣 ∈ { 𝐾} → (((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝐾) ∈ 𝐽))
3834, 37syl5ibrcom 248 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑣 ∈ { 𝐾} → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
3938ralrimiv 3150 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣 ∈ { 𝐾} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
40 imaco 5986 . . . . . . . . 9 (((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘))) “ 𝑢) = ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))
41 cnvco 5649 . . . . . . . . . . 11 ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = ((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘)))
4225adantlr 711 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) ∧ 𝑥𝑋) → (𝑥𝐵) ∈ 𝐾)
43 eqidd 2798 . . . . . . . . . . . . . 14 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑥𝑋 ↦ (𝑥𝐵)) = (𝑥𝑋 ↦ (𝑥𝐵)))
44 eqidd 2798 . . . . . . . . . . . . . 14 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑧 𝐾 ↦ (𝑧𝑘)) = (𝑧 𝐾 ↦ (𝑧𝑘)))
45 fveq1 6544 . . . . . . . . . . . . . 14 (𝑧 = (𝑥𝐵) → (𝑧𝑘) = ((𝑥𝐵)‘𝑘))
4642, 43, 44, 45fmptco 6761 . . . . . . . . . . . . 13 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = (𝑥𝑋 ↦ ((𝑥𝐵)‘𝑘)))
47 fvres 6564 . . . . . . . . . . . . . . 15 (𝑘𝐵 → ((𝑥𝐵)‘𝑘) = (𝑥𝑘))
4847ad2antrl 724 . . . . . . . . . . . . . 14 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝐵)‘𝑘) = (𝑥𝑘))
4948mpteq2dv 5063 . . . . . . . . . . . . 13 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑥𝑋 ↦ ((𝑥𝐵)‘𝑘)) = (𝑥𝑋 ↦ (𝑥𝑘)))
5046, 49eqtrd 2833 . . . . . . . . . . . 12 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = (𝑥𝑋 ↦ (𝑥𝑘)))
5150cnveqd 5639 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑧 𝐾 ↦ (𝑧𝑘)) ∘ (𝑥𝑋 ↦ (𝑥𝐵))) = (𝑥𝑋 ↦ (𝑥𝑘)))
5241, 51syl5eqr 2847 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘))) = (𝑥𝑋 ↦ (𝑥𝑘)))
5352imaeq1d 5812 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (((𝑥𝑋 ↦ (𝑥𝐵)) ∘ (𝑧 𝐾 ↦ (𝑧𝑘))) “ 𝑢) = ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢))
5440, 53syl5eqr 2847 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) = ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢))
55 simpl1 1184 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝐴𝑉)
56 simpl2 1185 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝐹:𝐴⟶Top)
57 simpl3 1186 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝐵𝐴)
58 simprl 767 . . . . . . . . . . 11 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝑘𝐵)
5957, 58sseldd 3896 . . . . . . . . . 10 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝑘𝐴)
605, 2ptpjcn 21907 . . . . . . . . . 10 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝑘𝐴) → (𝑥𝑋 ↦ (𝑥𝑘)) ∈ (𝐽 Cn (𝐹𝑘)))
6155, 56, 59, 60syl3anc 1364 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑥𝑋 ↦ (𝑥𝑘)) ∈ (𝐽 Cn (𝐹𝑘)))
62 simprr 769 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → 𝑢 ∈ (𝐹𝑘))
63 cnima 21561 . . . . . . . . 9 (((𝑥𝑋 ↦ (𝑥𝑘)) ∈ (𝐽 Cn (𝐹𝑘)) ∧ 𝑢 ∈ (𝐹𝑘)) → ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢) ∈ 𝐽)
6461, 62, 63syl2anc 584 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝑘)) “ 𝑢) ∈ 𝐽)
6554, 64eqeltrd 2885 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ 𝐽)
66 imaeq2 5809 . . . . . . . 8 (𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) = ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
6766eleq1d 2869 . . . . . . 7 (𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → (((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ((𝑥𝑋 ↦ (𝑥𝐵)) “ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ 𝐽))
6865, 67syl5ibrcom 248 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) ∧ (𝑘𝐵𝑢 ∈ (𝐹𝑘))) → (𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
6968rexlimdvva 3259 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
7069alrimiv 1909 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣(∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
71 eqid 2797 . . . . . . 7 (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) = (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))
7271rnmpo 7147 . . . . . 6 ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) = {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)}
7372raleqi 3375 . . . . 5 (∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣 ∈ {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
7412rexeqdv 3378 . . . . . . . 8 (𝑘𝐵 → (∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
75 eqeq1 2801 . . . . . . . . 9 (𝑦 = 𝑣 → (𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ 𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
7675rexbidv 3262 . . . . . . . 8 (𝑦 = 𝑣 → (∃𝑢 ∈ (𝐹𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
7774, 76sylan9bbr 511 . . . . . . 7 ((𝑦 = 𝑣𝑘𝐵) → (∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
7877rexbidva 3261 . . . . . 6 (𝑦 = 𝑣 → (∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) ↔ ∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))
7978ralab 3625 . . . . 5 (∀𝑣 ∈ {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣(∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
8073, 79bitri 276 . . . 4 (∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ ∀𝑣(∃𝑘𝐵𝑢 ∈ (𝐹𝑘)𝑣 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢) → ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
8170, 80sylibr 235 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
82 ralunb 4094 . . 3 (∀𝑣 ∈ ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ↔ (∀𝑣 ∈ { 𝐾} ((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽 ∧ ∀𝑣 ∈ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽))
8339, 81, 82sylanbrc 583 . 2 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ∀𝑣 ∈ ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)
845toptopon 21213 . . . 4 (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋))
8531, 84sylib 219 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐽 ∈ (TopOn‘𝑋))
86 snex 5230 . . . 4 { 𝐾} ∈ V
87 fvex 6558 . . . . . . . 8 ((𝐹𝐵)‘𝑘) ∈ V
8887abrexex 7526 . . . . . . 7 {𝑦 ∣ ∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V
8988rgenw 3119 . . . . . 6 𝑘𝐵 {𝑦 ∣ ∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V
90 abrexex2g 7528 . . . . . 6 ((𝐵 ∈ V ∧ ∀𝑘𝐵 {𝑦 ∣ ∃𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V) → {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V)
9117, 89, 90sylancl 586 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → {𝑦 ∣ ∃𝑘𝐵𝑢 ∈ ((𝐹𝐵)‘𝑘)𝑦 = ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)} ∈ V)
9272, 91syl5eqel 2889 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ V)
93 unexg 7336 . . . 4 (({ 𝐾} ∈ V ∧ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)) ∈ V) → ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))) ∈ V)
9486, 92, 93sylancr 587 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))) ∈ V)
95 eqid 2797 . . . . 5 𝐾 = 𝐾
9620, 95, 71ptval2 21897 . . . 4 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → 𝐾 = (topGen‘(fi‘({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))))))
9717, 19, 96syl2anc 584 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐾 = (topGen‘(fi‘({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢))))))
98 pttop 21878 . . . . . 6 ((𝐵 ∈ V ∧ (𝐹𝐵):𝐵⟶Top) → (∏t‘(𝐹𝐵)) ∈ Top)
9917, 19, 98syl2anc 584 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (∏t‘(𝐹𝐵)) ∈ Top)
10020, 99syl5eqel 2889 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐾 ∈ Top)
10195toptopon 21213 . . . 4 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
102100, 101sylib 219 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → 𝐾 ∈ (TopOn‘ 𝐾))
10385, 94, 97, 102subbascn 21550 . 2 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → ((𝑥𝑋 ↦ (𝑥𝐵)) ∈ (𝐽 Cn 𝐾) ↔ ((𝑥𝑋 ↦ (𝑥𝐵)):𝑋 𝐾 ∧ ∀𝑣 ∈ ({ 𝐾} ∪ ran (𝑘𝐵, 𝑢 ∈ ((𝐹𝐵)‘𝑘) ↦ ((𝑧 𝐾 ↦ (𝑧𝑘)) “ 𝑢)))((𝑥𝑋 ↦ (𝑥𝐵)) “ 𝑣) ∈ 𝐽)))
10426, 83, 103mpbir2and 709 1 ((𝐴𝑉𝐹:𝐴⟶Top ∧ 𝐵𝐴) → (𝑥𝑋 ↦ (𝑥𝐵)) ∈ (𝐽 Cn 𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080  wal 1523   = wceq 1525  wcel 2083  {cab 2777  wral 3107  wrex 3108  Vcvv 3440  cun 3863  wss 3865  {csn 4478   cuni 4751  cmpt 5047  ccnv 5449  ran crn 5451  cres 5452  cima 5453  ccom 5454  wf 6228  cfv 6232  (class class class)co 7023  cmpo 7025  Xcixp 8317  ficfi 8727  topGenctg 16544  tcpt 16545  Topctop 21189  TopOnctopon 21206   Cn ccn 21520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-iin 4834  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-ov 7026  df-oprab 7027  df-mpo 7028  df-om 7444  df-1st 7552  df-2nd 7553  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-oadd 7964  df-er 8146  df-map 8265  df-ixp 8318  df-en 8365  df-dom 8366  df-fin 8368  df-fi 8728  df-topgen 16550  df-pt 16551  df-top 21190  df-topon 21207  df-bases 21242  df-cn 21523
This theorem is referenced by:  ptunhmeo  22104  tmdgsum  22391
  Copyright terms: Public domain W3C validator