Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvmliftphtlem Structured version   Visualization version   GIF version

Theorem cvmliftphtlem 31598
Description: Lemma for cvmliftpht 31599. (Contributed by Mario Carneiro, 6-Jul-2015.)
Hypotheses
Ref Expression
cvmliftpht.b 𝐵 = 𝐶
cvmliftpht.m 𝑀 = (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
cvmliftpht.n 𝑁 = (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃))
cvmliftpht.f (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
cvmliftpht.p (𝜑𝑃𝐵)
cvmliftpht.e (𝜑 → (𝐹𝑃) = (𝐺‘0))
cvmliftphtlem.g (𝜑𝐺 ∈ (II Cn 𝐽))
cvmliftphtlem.h (𝜑𝐻 ∈ (II Cn 𝐽))
cvmliftphtlem.k (𝜑𝐾 ∈ (𝐺(PHtpy‘𝐽)𝐻))
cvmliftphtlem.a (𝜑𝐴 ∈ ((II ×t II) Cn 𝐶))
cvmliftphtlem.c (𝜑 → (𝐹𝐴) = 𝐾)
cvmliftphtlem.0 (𝜑 → (0𝐴0) = 𝑃)
Assertion
Ref Expression
cvmliftphtlem (𝜑𝐴 ∈ (𝑀(PHtpy‘𝐶)𝑁))
Distinct variable groups:   𝐴,𝑓   𝐵,𝑓   𝑓,𝐹   𝑓,𝐽   𝐶,𝑓   𝑓,𝐺   𝑓,𝐻   𝑃,𝑓
Allowed substitution hints:   𝜑(𝑓)   𝐾(𝑓)   𝑀(𝑓)   𝑁(𝑓)

Proof of Theorem cvmliftphtlem
Dummy variables 𝑠 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvmliftpht.b . . . 4 𝐵 = 𝐶
2 cvmliftpht.m . . . 4 𝑀 = (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
3 cvmliftpht.f . . . 4 (𝜑𝐹 ∈ (𝐶 CovMap 𝐽))
4 cvmliftphtlem.g . . . 4 (𝜑𝐺 ∈ (II Cn 𝐽))
5 cvmliftpht.p . . . 4 (𝜑𝑃𝐵)
6 cvmliftpht.e . . . 4 (𝜑 → (𝐹𝑃) = (𝐺‘0))
71, 2, 3, 4, 5, 6cvmliftiota 31582 . . 3 (𝜑 → (𝑀 ∈ (II Cn 𝐶) ∧ (𝐹𝑀) = 𝐺 ∧ (𝑀‘0) = 𝑃))
87simp1d 1136 . 2 (𝜑𝑀 ∈ (II Cn 𝐶))
9 cvmliftpht.n . . . 4 𝑁 = (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃))
10 cvmliftphtlem.h . . . 4 (𝜑𝐻 ∈ (II Cn 𝐽))
11 cvmliftphtlem.k . . . . . . 7 (𝜑𝐾 ∈ (𝐺(PHtpy‘𝐽)𝐻))
124, 10, 11phtpy01 22977 . . . . . 6 (𝜑 → ((𝐺‘0) = (𝐻‘0) ∧ (𝐺‘1) = (𝐻‘1)))
1312simpld 477 . . . . 5 (𝜑 → (𝐺‘0) = (𝐻‘0))
146, 13eqtrd 2786 . . . 4 (𝜑 → (𝐹𝑃) = (𝐻‘0))
151, 9, 3, 10, 5, 14cvmliftiota 31582 . . 3 (𝜑 → (𝑁 ∈ (II Cn 𝐶) ∧ (𝐹𝑁) = 𝐻 ∧ (𝑁‘0) = 𝑃))
1615simp1d 1136 . 2 (𝜑𝑁 ∈ (II Cn 𝐶))
17 cvmliftphtlem.a . 2 (𝜑𝐴 ∈ ((II ×t II) Cn 𝐶))
18 iitop 22876 . . . . . . . . . . . . . . . 16 II ∈ Top
19 iiuni 22877 . . . . . . . . . . . . . . . 16 (0[,]1) = II
2018, 18, 19, 19txunii 21590 . . . . . . . . . . . . . . 15 ((0[,]1) × (0[,]1)) = (II ×t II)
2120, 1cnf 21244 . . . . . . . . . . . . . 14 (𝐴 ∈ ((II ×t II) Cn 𝐶) → 𝐴:((0[,]1) × (0[,]1))⟶𝐵)
2217, 21syl 17 . . . . . . . . . . . . 13 (𝜑𝐴:((0[,]1) × (0[,]1))⟶𝐵)
23 0elunit 12475 . . . . . . . . . . . . . 14 0 ∈ (0[,]1)
24 opelxpi 5297 . . . . . . . . . . . . . 14 ((𝑠 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → ⟨𝑠, 0⟩ ∈ ((0[,]1) × (0[,]1)))
2523, 24mpan2 709 . . . . . . . . . . . . 13 (𝑠 ∈ (0[,]1) → ⟨𝑠, 0⟩ ∈ ((0[,]1) × (0[,]1)))
26 fvco3 6429 . . . . . . . . . . . . 13 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨𝑠, 0⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹𝐴)‘⟨𝑠, 0⟩) = (𝐹‘(𝐴‘⟨𝑠, 0⟩)))
2722, 25, 26syl2an 495 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹𝐴)‘⟨𝑠, 0⟩) = (𝐹‘(𝐴‘⟨𝑠, 0⟩)))
28 cvmliftphtlem.c . . . . . . . . . . . . . 14 (𝜑 → (𝐹𝐴) = 𝐾)
2928adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹𝐴) = 𝐾)
3029fveq1d 6346 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹𝐴)‘⟨𝑠, 0⟩) = (𝐾‘⟨𝑠, 0⟩))
3127, 30eqtr3d 2788 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(𝐴‘⟨𝑠, 0⟩)) = (𝐾‘⟨𝑠, 0⟩))
32 df-ov 6808 . . . . . . . . . . . 12 (𝑠𝐴0) = (𝐴‘⟨𝑠, 0⟩)
3332fveq2i 6347 . . . . . . . . . . 11 (𝐹‘(𝑠𝐴0)) = (𝐹‘(𝐴‘⟨𝑠, 0⟩))
34 df-ov 6808 . . . . . . . . . . 11 (𝑠𝐾0) = (𝐾‘⟨𝑠, 0⟩)
3531, 33, 343eqtr4g 2811 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(𝑠𝐴0)) = (𝑠𝐾0))
36 iitopon 22875 . . . . . . . . . . . . 13 II ∈ (TopOn‘(0[,]1))
3736a1i 11 . . . . . . . . . . . 12 (𝜑 → II ∈ (TopOn‘(0[,]1)))
384, 10phtpyhtpy 22974 . . . . . . . . . . . . 13 (𝜑 → (𝐺(PHtpy‘𝐽)𝐻) ⊆ (𝐺(II Htpy 𝐽)𝐻))
3938, 11sseldd 3737 . . . . . . . . . . . 12 (𝜑𝐾 ∈ (𝐺(II Htpy 𝐽)𝐻))
4037, 4, 10, 39htpyi 22966 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (0[,]1)) → ((𝑠𝐾0) = (𝐺𝑠) ∧ (𝑠𝐾1) = (𝐻𝑠)))
4140simpld 477 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0[,]1)) → (𝑠𝐾0) = (𝐺𝑠))
4235, 41eqtrd 2786 . . . . . . . . 9 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(𝑠𝐴0)) = (𝐺𝑠))
4342mpteq2dva 4888 . . . . . . . 8 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝐹‘(𝑠𝐴0))) = (𝑠 ∈ (0[,]1) ↦ (𝐺𝑠)))
44 fovrn 6961 . . . . . . . . . . 11 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵𝑠 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → (𝑠𝐴0) ∈ 𝐵)
4523, 44mp3an3 1554 . . . . . . . . . 10 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵𝑠 ∈ (0[,]1)) → (𝑠𝐴0) ∈ 𝐵)
4622, 45sylan 489 . . . . . . . . 9 ((𝜑𝑠 ∈ (0[,]1)) → (𝑠𝐴0) ∈ 𝐵)
47 eqidd 2753 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)))
48 cvmcn 31543 . . . . . . . . . . . 12 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐹 ∈ (𝐶 Cn 𝐽))
493, 48syl 17 . . . . . . . . . . 11 (𝜑𝐹 ∈ (𝐶 Cn 𝐽))
50 eqid 2752 . . . . . . . . . . . 12 𝐽 = 𝐽
511, 50cnf 21244 . . . . . . . . . . 11 (𝐹 ∈ (𝐶 Cn 𝐽) → 𝐹:𝐵 𝐽)
5249, 51syl 17 . . . . . . . . . 10 (𝜑𝐹:𝐵 𝐽)
5352feqmptd 6403 . . . . . . . . 9 (𝜑𝐹 = (𝑥𝐵 ↦ (𝐹𝑥)))
54 fveq2 6344 . . . . . . . . 9 (𝑥 = (𝑠𝐴0) → (𝐹𝑥) = (𝐹‘(𝑠𝐴0)))
5546, 47, 53, 54fmptco 6551 . . . . . . . 8 (𝜑 → (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = (𝑠 ∈ (0[,]1) ↦ (𝐹‘(𝑠𝐴0))))
5619, 50cnf 21244 . . . . . . . . . 10 (𝐺 ∈ (II Cn 𝐽) → 𝐺:(0[,]1)⟶ 𝐽)
574, 56syl 17 . . . . . . . . 9 (𝜑𝐺:(0[,]1)⟶ 𝐽)
5857feqmptd 6403 . . . . . . . 8 (𝜑𝐺 = (𝑠 ∈ (0[,]1) ↦ (𝐺𝑠)))
5943, 55, 583eqtr4d 2796 . . . . . . 7 (𝜑 → (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = 𝐺)
60 cvmliftphtlem.0 . . . . . . 7 (𝜑 → (0𝐴0) = 𝑃)
6137cnmptid 21658 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (0[,]1) ↦ 𝑠) ∈ (II Cn II))
6223a1i 11 . . . . . . . . . 10 (𝜑 → 0 ∈ (0[,]1))
6337, 37, 62cnmptc 21659 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (0[,]1) ↦ 0) ∈ (II Cn II))
6437, 61, 63, 17cnmpt12f 21663 . . . . . . . 8 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) ∈ (II Cn 𝐶))
651cvmlift 31580 . . . . . . . . 9 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐺 ∈ (II Cn 𝐽)) ∧ (𝑃𝐵 ∧ (𝐹𝑃) = (𝐺‘0))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
663, 4, 5, 6, 65syl22anc 1474 . . . . . . . 8 (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃))
67 coeq2 5428 . . . . . . . . . . 11 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) → (𝐹𝑓) = (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))))
6867eqeq1d 2754 . . . . . . . . . 10 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) → ((𝐹𝑓) = 𝐺 ↔ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = 𝐺))
69 fveq1 6343 . . . . . . . . . . . 12 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) → (𝑓‘0) = ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))‘0))
70 oveq1 6812 . . . . . . . . . . . . . 14 (𝑠 = 0 → (𝑠𝐴0) = (0𝐴0))
71 eqid 2752 . . . . . . . . . . . . . 14 (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))
72 ovex 6833 . . . . . . . . . . . . . 14 (0𝐴0) ∈ V
7370, 71, 72fvmpt 6436 . . . . . . . . . . . . 13 (0 ∈ (0[,]1) → ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))‘0) = (0𝐴0))
7423, 73ax-mp 5 . . . . . . . . . . . 12 ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))‘0) = (0𝐴0)
7569, 74syl6eq 2802 . . . . . . . . . . 11 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) → (𝑓‘0) = (0𝐴0))
7675eqeq1d 2754 . . . . . . . . . 10 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) → ((𝑓‘0) = 𝑃 ↔ (0𝐴0) = 𝑃))
7768, 76anbi12d 749 . . . . . . . . 9 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) → (((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃) ↔ ((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = 𝐺 ∧ (0𝐴0) = 𝑃)))
7877riota2 6788 . . . . . . . 8 (((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) ∈ (II Cn 𝐶) ∧ ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)) → (((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = 𝐺 ∧ (0𝐴0) = 𝑃) ↔ (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))))
7964, 66, 78syl2anc 696 . . . . . . 7 (𝜑 → (((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))) = 𝐺 ∧ (0𝐴0) = 𝑃) ↔ (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0))))
8059, 60, 79mpbi2and 994 . . . . . 6 (𝜑 → (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐺 ∧ (𝑓‘0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)))
812, 80syl5eq 2798 . . . . 5 (𝜑𝑀 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)))
8219, 1cnf 21244 . . . . . . 7 (𝑀 ∈ (II Cn 𝐶) → 𝑀:(0[,]1)⟶𝐵)
838, 82syl 17 . . . . . 6 (𝜑𝑀:(0[,]1)⟶𝐵)
8483feqmptd 6403 . . . . 5 (𝜑𝑀 = (𝑠 ∈ (0[,]1) ↦ (𝑀𝑠)))
8581, 84eqtr3d 2788 . . . 4 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) = (𝑠 ∈ (0[,]1) ↦ (𝑀𝑠)))
86 mpteqb 6453 . . . . 5 (∀𝑠 ∈ (0[,]1)(𝑠𝐴0) ∈ V → ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) = (𝑠 ∈ (0[,]1) ↦ (𝑀𝑠)) ↔ ∀𝑠 ∈ (0[,]1)(𝑠𝐴0) = (𝑀𝑠)))
87 ovexd 6835 . . . . 5 (𝑠 ∈ (0[,]1) → (𝑠𝐴0) ∈ V)
8886, 87mprg 3056 . . . 4 ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴0)) = (𝑠 ∈ (0[,]1) ↦ (𝑀𝑠)) ↔ ∀𝑠 ∈ (0[,]1)(𝑠𝐴0) = (𝑀𝑠))
8985, 88sylib 208 . . 3 (𝜑 → ∀𝑠 ∈ (0[,]1)(𝑠𝐴0) = (𝑀𝑠))
9089r19.21bi 3062 . 2 ((𝜑𝑠 ∈ (0[,]1)) → (𝑠𝐴0) = (𝑀𝑠))
91 1elunit 12476 . . . . . . . . . . . . . 14 1 ∈ (0[,]1)
92 opelxpi 5297 . . . . . . . . . . . . . 14 ((𝑠 ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → ⟨𝑠, 1⟩ ∈ ((0[,]1) × (0[,]1)))
9391, 92mpan2 709 . . . . . . . . . . . . 13 (𝑠 ∈ (0[,]1) → ⟨𝑠, 1⟩ ∈ ((0[,]1) × (0[,]1)))
94 fvco3 6429 . . . . . . . . . . . . 13 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨𝑠, 1⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹𝐴)‘⟨𝑠, 1⟩) = (𝐹‘(𝐴‘⟨𝑠, 1⟩)))
9522, 93, 94syl2an 495 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹𝐴)‘⟨𝑠, 1⟩) = (𝐹‘(𝐴‘⟨𝑠, 1⟩)))
9629fveq1d 6346 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹𝐴)‘⟨𝑠, 1⟩) = (𝐾‘⟨𝑠, 1⟩))
9795, 96eqtr3d 2788 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(𝐴‘⟨𝑠, 1⟩)) = (𝐾‘⟨𝑠, 1⟩))
98 df-ov 6808 . . . . . . . . . . . 12 (𝑠𝐴1) = (𝐴‘⟨𝑠, 1⟩)
9998fveq2i 6347 . . . . . . . . . . 11 (𝐹‘(𝑠𝐴1)) = (𝐹‘(𝐴‘⟨𝑠, 1⟩))
100 df-ov 6808 . . . . . . . . . . 11 (𝑠𝐾1) = (𝐾‘⟨𝑠, 1⟩)
10197, 99, 1003eqtr4g 2811 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(𝑠𝐴1)) = (𝑠𝐾1))
10240simprd 482 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0[,]1)) → (𝑠𝐾1) = (𝐻𝑠))
103101, 102eqtrd 2786 . . . . . . . . 9 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(𝑠𝐴1)) = (𝐻𝑠))
104103mpteq2dva 4888 . . . . . . . 8 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝐹‘(𝑠𝐴1))) = (𝑠 ∈ (0[,]1) ↦ (𝐻𝑠)))
105 fovrn 6961 . . . . . . . . . . 11 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵𝑠 ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → (𝑠𝐴1) ∈ 𝐵)
10691, 105mp3an3 1554 . . . . . . . . . 10 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵𝑠 ∈ (0[,]1)) → (𝑠𝐴1) ∈ 𝐵)
10722, 106sylan 489 . . . . . . . . 9 ((𝜑𝑠 ∈ (0[,]1)) → (𝑠𝐴1) ∈ 𝐵)
108 eqidd 2753 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)))
109 fveq2 6344 . . . . . . . . 9 (𝑥 = (𝑠𝐴1) → (𝐹𝑥) = (𝐹‘(𝑠𝐴1)))
110107, 108, 53, 109fmptco 6551 . . . . . . . 8 (𝜑 → (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = (𝑠 ∈ (0[,]1) ↦ (𝐹‘(𝑠𝐴1))))
11119, 50cnf 21244 . . . . . . . . . 10 (𝐻 ∈ (II Cn 𝐽) → 𝐻:(0[,]1)⟶ 𝐽)
11210, 111syl 17 . . . . . . . . 9 (𝜑𝐻:(0[,]1)⟶ 𝐽)
113112feqmptd 6403 . . . . . . . 8 (𝜑𝐻 = (𝑠 ∈ (0[,]1) ↦ (𝐻𝑠)))
114104, 110, 1133eqtr4d 2796 . . . . . . 7 (𝜑 → (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = 𝐻)
115 iiconn 22883 . . . . . . . . . . . . 13 II ∈ Conn
116115a1i 11 . . . . . . . . . . . 12 (𝜑 → II ∈ Conn)
117 iinllyconn 31535 . . . . . . . . . . . . 13 II ∈ 𝑛-Locally Conn
118117a1i 11 . . . . . . . . . . . 12 (𝜑 → II ∈ 𝑛-Locally Conn)
11937, 63, 61, 17cnmpt12f 21663 . . . . . . . . . . . 12 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) ∈ (II Cn 𝐶))
120 cvmtop1 31541 . . . . . . . . . . . . . . 15 (𝐹 ∈ (𝐶 CovMap 𝐽) → 𝐶 ∈ Top)
1213, 120syl 17 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ Top)
1221toptopon 20916 . . . . . . . . . . . . . 14 (𝐶 ∈ Top ↔ 𝐶 ∈ (TopOn‘𝐵))
123121, 122sylib 208 . . . . . . . . . . . . 13 (𝜑𝐶 ∈ (TopOn‘𝐵))
124 ffvelrn 6512 . . . . . . . . . . . . . 14 ((𝑀:(0[,]1)⟶𝐵 ∧ 0 ∈ (0[,]1)) → (𝑀‘0) ∈ 𝐵)
12583, 23, 124sylancl 697 . . . . . . . . . . . . 13 (𝜑 → (𝑀‘0) ∈ 𝐵)
126 cnconst2 21281 . . . . . . . . . . . . 13 ((II ∈ (TopOn‘(0[,]1)) ∧ 𝐶 ∈ (TopOn‘𝐵) ∧ (𝑀‘0) ∈ 𝐵) → ((0[,]1) × {(𝑀‘0)}) ∈ (II Cn 𝐶))
12737, 123, 125, 126syl3anc 1473 . . . . . . . . . . . 12 (𝜑 → ((0[,]1) × {(𝑀‘0)}) ∈ (II Cn 𝐶))
1284, 10, 11phtpyi 22976 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (0[,]1)) → ((0𝐾𝑠) = (𝐺‘0) ∧ (1𝐾𝑠) = (𝐺‘1)))
129128simpld 477 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (0[,]1)) → (0𝐾𝑠) = (𝐺‘0))
130 opelxpi 5297 . . . . . . . . . . . . . . . . . . . 20 ((0 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → ⟨0, 𝑠⟩ ∈ ((0[,]1) × (0[,]1)))
13123, 130mpan 708 . . . . . . . . . . . . . . . . . . 19 (𝑠 ∈ (0[,]1) → ⟨0, 𝑠⟩ ∈ ((0[,]1) × (0[,]1)))
132 fvco3 6429 . . . . . . . . . . . . . . . . . . 19 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨0, 𝑠⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹𝐴)‘⟨0, 𝑠⟩) = (𝐹‘(𝐴‘⟨0, 𝑠⟩)))
13322, 131, 132syl2an 495 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹𝐴)‘⟨0, 𝑠⟩) = (𝐹‘(𝐴‘⟨0, 𝑠⟩)))
13429fveq1d 6346 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹𝐴)‘⟨0, 𝑠⟩) = (𝐾‘⟨0, 𝑠⟩))
135133, 134eqtr3d 2788 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(𝐴‘⟨0, 𝑠⟩)) = (𝐾‘⟨0, 𝑠⟩))
136 df-ov 6808 . . . . . . . . . . . . . . . . . 18 (0𝐴𝑠) = (𝐴‘⟨0, 𝑠⟩)
137136fveq2i 6347 . . . . . . . . . . . . . . . . 17 (𝐹‘(0𝐴𝑠)) = (𝐹‘(𝐴‘⟨0, 𝑠⟩))
138 df-ov 6808 . . . . . . . . . . . . . . . . 17 (0𝐾𝑠) = (𝐾‘⟨0, 𝑠⟩)
139135, 137, 1383eqtr4g 2811 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(0𝐴𝑠)) = (0𝐾𝑠))
1407simp3d 1138 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀‘0) = 𝑃)
141140adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑠 ∈ (0[,]1)) → (𝑀‘0) = 𝑃)
142141fveq2d 6348 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(𝑀‘0)) = (𝐹𝑃))
1436adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹𝑃) = (𝐺‘0))
144142, 143eqtrd 2786 . . . . . . . . . . . . . . . 16 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(𝑀‘0)) = (𝐺‘0))
145129, 139, 1443eqtr4d 2796 . . . . . . . . . . . . . . 15 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(0𝐴𝑠)) = (𝐹‘(𝑀‘0)))
146145mpteq2dva 4888 . . . . . . . . . . . . . 14 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝐹‘(0𝐴𝑠))) = (𝑠 ∈ (0[,]1) ↦ (𝐹‘(𝑀‘0))))
147 fconstmpt 5312 . . . . . . . . . . . . . 14 ((0[,]1) × {(𝐹‘(𝑀‘0))}) = (𝑠 ∈ (0[,]1) ↦ (𝐹‘(𝑀‘0)))
148146, 147syl6eqr 2804 . . . . . . . . . . . . 13 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝐹‘(0𝐴𝑠))) = ((0[,]1) × {(𝐹‘(𝑀‘0))}))
149 fovrn 6961 . . . . . . . . . . . . . . . 16 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵 ∧ 0 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → (0𝐴𝑠) ∈ 𝐵)
15023, 149mp3an2 1553 . . . . . . . . . . . . . . 15 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵𝑠 ∈ (0[,]1)) → (0𝐴𝑠) ∈ 𝐵)
15122, 150sylan 489 . . . . . . . . . . . . . 14 ((𝜑𝑠 ∈ (0[,]1)) → (0𝐴𝑠) ∈ 𝐵)
152 eqidd 2753 . . . . . . . . . . . . . 14 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)))
153 fveq2 6344 . . . . . . . . . . . . . 14 (𝑥 = (0𝐴𝑠) → (𝐹𝑥) = (𝐹‘(0𝐴𝑠)))
154151, 152, 53, 153fmptco 6551 . . . . . . . . . . . . 13 (𝜑 → (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))) = (𝑠 ∈ (0[,]1) ↦ (𝐹‘(0𝐴𝑠))))
155 ffn 6198 . . . . . . . . . . . . . . 15 (𝐹:𝐵 𝐽𝐹 Fn 𝐵)
15652, 155syl 17 . . . . . . . . . . . . . 14 (𝜑𝐹 Fn 𝐵)
157 fcoconst 6556 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐵 ∧ (𝑀‘0) ∈ 𝐵) → (𝐹 ∘ ((0[,]1) × {(𝑀‘0)})) = ((0[,]1) × {(𝐹‘(𝑀‘0))}))
158156, 125, 157syl2anc 696 . . . . . . . . . . . . 13 (𝜑 → (𝐹 ∘ ((0[,]1) × {(𝑀‘0)})) = ((0[,]1) × {(𝐹‘(𝑀‘0))}))
159148, 154, 1583eqtr4d 2796 . . . . . . . . . . . 12 (𝜑 → (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))) = (𝐹 ∘ ((0[,]1) × {(𝑀‘0)})))
16060, 140eqtr4d 2789 . . . . . . . . . . . . 13 (𝜑 → (0𝐴0) = (𝑀‘0))
161 oveq2 6813 . . . . . . . . . . . . . . 15 (𝑠 = 0 → (0𝐴𝑠) = (0𝐴0))
162 eqid 2752 . . . . . . . . . . . . . . 15 (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))
163161, 162, 72fvmpt 6436 . . . . . . . . . . . . . 14 (0 ∈ (0[,]1) → ((𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))‘0) = (0𝐴0))
16423, 163ax-mp 5 . . . . . . . . . . . . 13 ((𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))‘0) = (0𝐴0)
165 fvex 6354 . . . . . . . . . . . . . . 15 (𝑀‘0) ∈ V
166165fvconst2 6625 . . . . . . . . . . . . . 14 (0 ∈ (0[,]1) → (((0[,]1) × {(𝑀‘0)})‘0) = (𝑀‘0))
16723, 166ax-mp 5 . . . . . . . . . . . . 13 (((0[,]1) × {(𝑀‘0)})‘0) = (𝑀‘0)
168160, 164, 1673eqtr4g 2811 . . . . . . . . . . . 12 (𝜑 → ((𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠))‘0) = (((0[,]1) × {(𝑀‘0)})‘0))
1691, 19, 3, 116, 118, 62, 119, 127, 159, 168cvmliftmoi 31564 . . . . . . . . . . 11 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = ((0[,]1) × {(𝑀‘0)}))
170 fconstmpt 5312 . . . . . . . . . . 11 ((0[,]1) × {(𝑀‘0)}) = (𝑠 ∈ (0[,]1) ↦ (𝑀‘0))
171169, 170syl6eq 2802 . . . . . . . . . 10 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (𝑀‘0)))
172 mpteqb 6453 . . . . . . . . . . 11 (∀𝑠 ∈ (0[,]1)(0𝐴𝑠) ∈ V → ((𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (𝑀‘0)) ↔ ∀𝑠 ∈ (0[,]1)(0𝐴𝑠) = (𝑀‘0)))
173 ovexd 6835 . . . . . . . . . . 11 (𝑠 ∈ (0[,]1) → (0𝐴𝑠) ∈ V)
174172, 173mprg 3056 . . . . . . . . . 10 ((𝑠 ∈ (0[,]1) ↦ (0𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (𝑀‘0)) ↔ ∀𝑠 ∈ (0[,]1)(0𝐴𝑠) = (𝑀‘0))
175171, 174sylib 208 . . . . . . . . 9 (𝜑 → ∀𝑠 ∈ (0[,]1)(0𝐴𝑠) = (𝑀‘0))
176 oveq2 6813 . . . . . . . . . . 11 (𝑠 = 1 → (0𝐴𝑠) = (0𝐴1))
177176eqeq1d 2754 . . . . . . . . . 10 (𝑠 = 1 → ((0𝐴𝑠) = (𝑀‘0) ↔ (0𝐴1) = (𝑀‘0)))
178177rspcv 3437 . . . . . . . . 9 (1 ∈ (0[,]1) → (∀𝑠 ∈ (0[,]1)(0𝐴𝑠) = (𝑀‘0) → (0𝐴1) = (𝑀‘0)))
17991, 175, 178mpsyl 68 . . . . . . . 8 (𝜑 → (0𝐴1) = (𝑀‘0))
180179, 140eqtrd 2786 . . . . . . 7 (𝜑 → (0𝐴1) = 𝑃)
18191a1i 11 . . . . . . . . . 10 (𝜑 → 1 ∈ (0[,]1))
18237, 37, 181cnmptc 21659 . . . . . . . . 9 (𝜑 → (𝑠 ∈ (0[,]1) ↦ 1) ∈ (II Cn II))
18337, 61, 182, 17cnmpt12f 21663 . . . . . . . 8 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) ∈ (II Cn 𝐶))
1841cvmlift 31580 . . . . . . . . 9 (((𝐹 ∈ (𝐶 CovMap 𝐽) ∧ 𝐻 ∈ (II Cn 𝐽)) ∧ (𝑃𝐵 ∧ (𝐹𝑃) = (𝐻‘0))) → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃))
1853, 10, 5, 14, 184syl22anc 1474 . . . . . . . 8 (𝜑 → ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃))
186 coeq2 5428 . . . . . . . . . . 11 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) → (𝐹𝑓) = (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))))
187186eqeq1d 2754 . . . . . . . . . 10 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) → ((𝐹𝑓) = 𝐻 ↔ (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = 𝐻))
188 fveq1 6343 . . . . . . . . . . . 12 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) → (𝑓‘0) = ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))‘0))
189 oveq1 6812 . . . . . . . . . . . . . 14 (𝑠 = 0 → (𝑠𝐴1) = (0𝐴1))
190 eqid 2752 . . . . . . . . . . . . . 14 (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))
191 ovex 6833 . . . . . . . . . . . . . 14 (0𝐴1) ∈ V
192189, 190, 191fvmpt 6436 . . . . . . . . . . . . 13 (0 ∈ (0[,]1) → ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))‘0) = (0𝐴1))
19323, 192ax-mp 5 . . . . . . . . . . . 12 ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))‘0) = (0𝐴1)
194188, 193syl6eq 2802 . . . . . . . . . . 11 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) → (𝑓‘0) = (0𝐴1))
195194eqeq1d 2754 . . . . . . . . . 10 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) → ((𝑓‘0) = 𝑃 ↔ (0𝐴1) = 𝑃))
196187, 195anbi12d 749 . . . . . . . . 9 (𝑓 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) → (((𝐹𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃) ↔ ((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = 𝐻 ∧ (0𝐴1) = 𝑃)))
197196riota2 6788 . . . . . . . 8 (((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) ∈ (II Cn 𝐶) ∧ ∃!𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃)) → (((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = 𝐻 ∧ (0𝐴1) = 𝑃) ↔ (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))))
198183, 185, 197syl2anc 696 . . . . . . 7 (𝜑 → (((𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))) = 𝐻 ∧ (0𝐴1) = 𝑃) ↔ (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1))))
199114, 180, 198mpbi2and 994 . . . . . 6 (𝜑 → (𝑓 ∈ (II Cn 𝐶)((𝐹𝑓) = 𝐻 ∧ (𝑓‘0) = 𝑃)) = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)))
2009, 199syl5eq 2798 . . . . 5 (𝜑𝑁 = (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)))
20119, 1cnf 21244 . . . . . . 7 (𝑁 ∈ (II Cn 𝐶) → 𝑁:(0[,]1)⟶𝐵)
20216, 201syl 17 . . . . . 6 (𝜑𝑁:(0[,]1)⟶𝐵)
203202feqmptd 6403 . . . . 5 (𝜑𝑁 = (𝑠 ∈ (0[,]1) ↦ (𝑁𝑠)))
204200, 203eqtr3d 2788 . . . 4 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) = (𝑠 ∈ (0[,]1) ↦ (𝑁𝑠)))
205 mpteqb 6453 . . . . 5 (∀𝑠 ∈ (0[,]1)(𝑠𝐴1) ∈ V → ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) = (𝑠 ∈ (0[,]1) ↦ (𝑁𝑠)) ↔ ∀𝑠 ∈ (0[,]1)(𝑠𝐴1) = (𝑁𝑠)))
206 ovexd 6835 . . . . 5 (𝑠 ∈ (0[,]1) → (𝑠𝐴1) ∈ V)
207205, 206mprg 3056 . . . 4 ((𝑠 ∈ (0[,]1) ↦ (𝑠𝐴1)) = (𝑠 ∈ (0[,]1) ↦ (𝑁𝑠)) ↔ ∀𝑠 ∈ (0[,]1)(𝑠𝐴1) = (𝑁𝑠))
208204, 207sylib 208 . . 3 (𝜑 → ∀𝑠 ∈ (0[,]1)(𝑠𝐴1) = (𝑁𝑠))
209208r19.21bi 3062 . 2 ((𝜑𝑠 ∈ (0[,]1)) → (𝑠𝐴1) = (𝑁𝑠))
210175r19.21bi 3062 . 2 ((𝜑𝑠 ∈ (0[,]1)) → (0𝐴𝑠) = (𝑀‘0))
21137, 182, 61, 17cnmpt12f 21663 . . . . . 6 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) ∈ (II Cn 𝐶))
212 ffvelrn 6512 . . . . . . . 8 ((𝑀:(0[,]1)⟶𝐵 ∧ 1 ∈ (0[,]1)) → (𝑀‘1) ∈ 𝐵)
21383, 91, 212sylancl 697 . . . . . . 7 (𝜑 → (𝑀‘1) ∈ 𝐵)
214 cnconst2 21281 . . . . . . 7 ((II ∈ (TopOn‘(0[,]1)) ∧ 𝐶 ∈ (TopOn‘𝐵) ∧ (𝑀‘1) ∈ 𝐵) → ((0[,]1) × {(𝑀‘1)}) ∈ (II Cn 𝐶))
21537, 123, 213, 214syl3anc 1473 . . . . . 6 (𝜑 → ((0[,]1) × {(𝑀‘1)}) ∈ (II Cn 𝐶))
216 opelxpi 5297 . . . . . . . . . . . . . 14 ((1 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → ⟨1, 𝑠⟩ ∈ ((0[,]1) × (0[,]1)))
21791, 216mpan 708 . . . . . . . . . . . . 13 (𝑠 ∈ (0[,]1) → ⟨1, 𝑠⟩ ∈ ((0[,]1) × (0[,]1)))
218 fvco3 6429 . . . . . . . . . . . . 13 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵 ∧ ⟨1, 𝑠⟩ ∈ ((0[,]1) × (0[,]1))) → ((𝐹𝐴)‘⟨1, 𝑠⟩) = (𝐹‘(𝐴‘⟨1, 𝑠⟩)))
21922, 217, 218syl2an 495 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹𝐴)‘⟨1, 𝑠⟩) = (𝐹‘(𝐴‘⟨1, 𝑠⟩)))
22029fveq1d 6346 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹𝐴)‘⟨1, 𝑠⟩) = (𝐾‘⟨1, 𝑠⟩))
221219, 220eqtr3d 2788 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(𝐴‘⟨1, 𝑠⟩)) = (𝐾‘⟨1, 𝑠⟩))
222 df-ov 6808 . . . . . . . . . . . 12 (1𝐴𝑠) = (𝐴‘⟨1, 𝑠⟩)
223222fveq2i 6347 . . . . . . . . . . 11 (𝐹‘(1𝐴𝑠)) = (𝐹‘(𝐴‘⟨1, 𝑠⟩))
224 df-ov 6808 . . . . . . . . . . 11 (1𝐾𝑠) = (𝐾‘⟨1, 𝑠⟩)
225221, 223, 2243eqtr4g 2811 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(1𝐴𝑠)) = (1𝐾𝑠))
226128simprd 482 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0[,]1)) → (1𝐾𝑠) = (𝐺‘1))
2277simp2d 1137 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑀) = 𝐺)
228227adantr 472 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹𝑀) = 𝐺)
229228fveq1d 6346 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹𝑀)‘1) = (𝐺‘1))
23083adantr 472 . . . . . . . . . . . 12 ((𝜑𝑠 ∈ (0[,]1)) → 𝑀:(0[,]1)⟶𝐵)
231 fvco3 6429 . . . . . . . . . . . 12 ((𝑀:(0[,]1)⟶𝐵 ∧ 1 ∈ (0[,]1)) → ((𝐹𝑀)‘1) = (𝐹‘(𝑀‘1)))
232230, 91, 231sylancl 697 . . . . . . . . . . 11 ((𝜑𝑠 ∈ (0[,]1)) → ((𝐹𝑀)‘1) = (𝐹‘(𝑀‘1)))
233229, 232eqtr3d 2788 . . . . . . . . . 10 ((𝜑𝑠 ∈ (0[,]1)) → (𝐺‘1) = (𝐹‘(𝑀‘1)))
234225, 226, 2333eqtrd 2790 . . . . . . . . 9 ((𝜑𝑠 ∈ (0[,]1)) → (𝐹‘(1𝐴𝑠)) = (𝐹‘(𝑀‘1)))
235234mpteq2dva 4888 . . . . . . . 8 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝐹‘(1𝐴𝑠))) = (𝑠 ∈ (0[,]1) ↦ (𝐹‘(𝑀‘1))))
236 fconstmpt 5312 . . . . . . . 8 ((0[,]1) × {(𝐹‘(𝑀‘1))}) = (𝑠 ∈ (0[,]1) ↦ (𝐹‘(𝑀‘1)))
237235, 236syl6eqr 2804 . . . . . . 7 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (𝐹‘(1𝐴𝑠))) = ((0[,]1) × {(𝐹‘(𝑀‘1))}))
238 fovrn 6961 . . . . . . . . . 10 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵 ∧ 1 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → (1𝐴𝑠) ∈ 𝐵)
23991, 238mp3an2 1553 . . . . . . . . 9 ((𝐴:((0[,]1) × (0[,]1))⟶𝐵𝑠 ∈ (0[,]1)) → (1𝐴𝑠) ∈ 𝐵)
24022, 239sylan 489 . . . . . . . 8 ((𝜑𝑠 ∈ (0[,]1)) → (1𝐴𝑠) ∈ 𝐵)
241 eqidd 2753 . . . . . . . 8 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)))
242 fveq2 6344 . . . . . . . 8 (𝑥 = (1𝐴𝑠) → (𝐹𝑥) = (𝐹‘(1𝐴𝑠)))
243240, 241, 53, 242fmptco 6551 . . . . . . 7 (𝜑 → (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))) = (𝑠 ∈ (0[,]1) ↦ (𝐹‘(1𝐴𝑠))))
244 fcoconst 6556 . . . . . . . 8 ((𝐹 Fn 𝐵 ∧ (𝑀‘1) ∈ 𝐵) → (𝐹 ∘ ((0[,]1) × {(𝑀‘1)})) = ((0[,]1) × {(𝐹‘(𝑀‘1))}))
245156, 213, 244syl2anc 696 . . . . . . 7 (𝜑 → (𝐹 ∘ ((0[,]1) × {(𝑀‘1)})) = ((0[,]1) × {(𝐹‘(𝑀‘1))}))
246237, 243, 2453eqtr4d 2796 . . . . . 6 (𝜑 → (𝐹 ∘ (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))) = (𝐹 ∘ ((0[,]1) × {(𝑀‘1)})))
247 oveq1 6812 . . . . . . . . . 10 (𝑠 = 1 → (𝑠𝐴0) = (1𝐴0))
248 fveq2 6344 . . . . . . . . . 10 (𝑠 = 1 → (𝑀𝑠) = (𝑀‘1))
249247, 248eqeq12d 2767 . . . . . . . . 9 (𝑠 = 1 → ((𝑠𝐴0) = (𝑀𝑠) ↔ (1𝐴0) = (𝑀‘1)))
250249rspcv 3437 . . . . . . . 8 (1 ∈ (0[,]1) → (∀𝑠 ∈ (0[,]1)(𝑠𝐴0) = (𝑀𝑠) → (1𝐴0) = (𝑀‘1)))
25191, 89, 250mpsyl 68 . . . . . . 7 (𝜑 → (1𝐴0) = (𝑀‘1))
252 oveq2 6813 . . . . . . . . 9 (𝑠 = 0 → (1𝐴𝑠) = (1𝐴0))
253 eqid 2752 . . . . . . . . 9 (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))
254 ovex 6833 . . . . . . . . 9 (1𝐴0) ∈ V
255252, 253, 254fvmpt 6436 . . . . . . . 8 (0 ∈ (0[,]1) → ((𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))‘0) = (1𝐴0))
25623, 255ax-mp 5 . . . . . . 7 ((𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))‘0) = (1𝐴0)
257 fvex 6354 . . . . . . . . 9 (𝑀‘1) ∈ V
258257fvconst2 6625 . . . . . . . 8 (0 ∈ (0[,]1) → (((0[,]1) × {(𝑀‘1)})‘0) = (𝑀‘1))
25923, 258ax-mp 5 . . . . . . 7 (((0[,]1) × {(𝑀‘1)})‘0) = (𝑀‘1)
260251, 256, 2593eqtr4g 2811 . . . . . 6 (𝜑 → ((𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠))‘0) = (((0[,]1) × {(𝑀‘1)})‘0))
2611, 19, 3, 116, 118, 62, 211, 215, 246, 260cvmliftmoi 31564 . . . . 5 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = ((0[,]1) × {(𝑀‘1)}))
262 fconstmpt 5312 . . . . 5 ((0[,]1) × {(𝑀‘1)}) = (𝑠 ∈ (0[,]1) ↦ (𝑀‘1))
263261, 262syl6eq 2802 . . . 4 (𝜑 → (𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (𝑀‘1)))
264 mpteqb 6453 . . . . 5 (∀𝑠 ∈ (0[,]1)(1𝐴𝑠) ∈ V → ((𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (𝑀‘1)) ↔ ∀𝑠 ∈ (0[,]1)(1𝐴𝑠) = (𝑀‘1)))
265 ovexd 6835 . . . . 5 (𝑠 ∈ (0[,]1) → (1𝐴𝑠) ∈ V)
266264, 265mprg 3056 . . . 4 ((𝑠 ∈ (0[,]1) ↦ (1𝐴𝑠)) = (𝑠 ∈ (0[,]1) ↦ (𝑀‘1)) ↔ ∀𝑠 ∈ (0[,]1)(1𝐴𝑠) = (𝑀‘1))
267263, 266sylib 208 . . 3 (𝜑 → ∀𝑠 ∈ (0[,]1)(1𝐴𝑠) = (𝑀‘1))
268267r19.21bi 3062 . 2 ((𝜑𝑠 ∈ (0[,]1)) → (1𝐴𝑠) = (𝑀‘1))
2698, 16, 17, 90, 209, 210, 268isphtpy2d 22979 1 (𝜑𝐴 ∈ (𝑀(PHtpy‘𝐶)𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1624  wcel 2131  wral 3042  ∃!wreu 3044  Vcvv 3332  {csn 4313  cop 4319   cuni 4580  cmpt 4873   × cxp 5256  ccom 5262   Fn wfn 6036  wf 6037  cfv 6041  crio 6765  (class class class)co 6805  0cc0 10120  1c1 10121  [,]cicc 12363  Topctop 20892  TopOnctopon 20909   Cn ccn 21222  Conncconn 21408  𝑛-Locally cnlly 21462   ×t ctx 21557  IIcii 22871   Htpy chtpy 22959  PHtpycphtpy 22960   CovMap ccvm 31536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-inf2 8703  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197  ax-pre-sup 10198  ax-addf 10199  ax-mulf 10200
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-fal 1630  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-iin 4667  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-se 5218  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-isom 6050  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-of 7054  df-om 7223  df-1st 7325  df-2nd 7326  df-supp 7456  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-2o 7722  df-oadd 7725  df-er 7903  df-ec 7905  df-map 8017  df-ixp 8067  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-fsupp 8433  df-fi 8474  df-sup 8505  df-inf 8506  df-oi 8572  df-card 8947  df-cda 9174  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-div 10869  df-nn 11205  df-2 11263  df-3 11264  df-4 11265  df-5 11266  df-6 11267  df-7 11268  df-8 11269  df-9 11270  df-n0 11477  df-z 11562  df-dec 11678  df-uz 11872  df-q 11974  df-rp 12018  df-xneg 12131  df-xadd 12132  df-xmul 12133  df-ioo 12364  df-ico 12366  df-icc 12367  df-fz 12512  df-fzo 12652  df-fl 12779  df-seq 12988  df-exp 13047  df-hash 13304  df-cj 14030  df-re 14031  df-im 14032  df-sqrt 14166  df-abs 14167  df-clim 14410  df-sum 14608  df-struct 16053  df-ndx 16054  df-slot 16055  df-base 16057  df-sets 16058  df-ress 16059  df-plusg 16148  df-mulr 16149  df-starv 16150  df-sca 16151  df-vsca 16152  df-ip 16153  df-tset 16154  df-ple 16155  df-ds 16158  df-unif 16159  df-hom 16160  df-cco 16161  df-rest 16277  df-topn 16278  df-0g 16296  df-gsum 16297  df-topgen 16298  df-pt 16299  df-prds 16302  df-xrs 16356  df-qtop 16361  df-imas 16362  df-xps 16364  df-mre 16440  df-mrc 16441  df-acs 16443  df-mgm 17435  df-sgrp 17477  df-mnd 17488  df-submnd 17529  df-mulg 17734  df-cntz 17942  df-cmn 18387  df-psmet 19932  df-xmet 19933  df-met 19934  df-bl 19935  df-mopn 19936  df-cnfld 19941  df-top 20893  df-topon 20910  df-topsp 20931  df-bases 20944  df-cld 21017  df-ntr 21018  df-cls 21019  df-nei 21096  df-cn 21225  df-cnp 21226  df-cmp 21384  df-conn 21409  df-lly 21463  df-nlly 21464  df-tx 21559  df-hmeo 21752  df-xms 22318  df-ms 22319  df-tms 22320  df-ii 22873  df-htpy 22962  df-phtpy 22963  df-phtpc 22984  df-pconn 31502  df-sconn 31503  df-cvm 31537
This theorem is referenced by:  cvmliftpht  31599
  Copyright terms: Public domain W3C validator