Step |
Hyp |
Ref |
Expression |
1 |
|
cvmlift3.b |
⊢ 𝐵 = ∪ 𝐶 |
2 |
|
cvmlift3.y |
⊢ 𝑌 = ∪ 𝐾 |
3 |
|
cvmlift3.f |
⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ) |
4 |
|
cvmlift3.k |
⊢ ( 𝜑 → 𝐾 ∈ SConn ) |
5 |
|
cvmlift3.l |
⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally PConn ) |
6 |
|
cvmlift3.o |
⊢ ( 𝜑 → 𝑂 ∈ 𝑌 ) |
7 |
|
cvmlift3.g |
⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) ) |
8 |
|
cvmlift3.p |
⊢ ( 𝜑 → 𝑃 ∈ 𝐵 ) |
9 |
|
cvmlift3.e |
⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) ) |
10 |
|
cvmlift3.h |
⊢ 𝐻 = ( 𝑥 ∈ 𝑌 ↦ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) ) |
11 |
|
eqid |
⊢ ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) |
12 |
1 2 3 4 5 6 7 8 9 10
|
cvmlift3lem4 |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( ( 𝐻 ‘ 𝑦 ) = ( 𝐻 ‘ 𝑦 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑦 ) ) ) ) |
13 |
11 12
|
mpbii |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑦 ) ) ) |
14 |
|
df-3an |
⊢ ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑦 ) ) ↔ ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑦 ) ) ) |
15 |
|
eqid |
⊢ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) |
16 |
3
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ) |
17 |
|
simplr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → 𝑓 ∈ ( II Cn 𝐾 ) ) |
18 |
7
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) ) |
19 |
|
cnco |
⊢ ( ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝐺 ∘ 𝑓 ) ∈ ( II Cn 𝐽 ) ) |
20 |
17 18 19
|
syl2anc |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( 𝐺 ∘ 𝑓 ) ∈ ( II Cn 𝐽 ) ) |
21 |
8
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → 𝑃 ∈ 𝐵 ) |
22 |
|
simprl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( 𝑓 ‘ 0 ) = 𝑂 ) |
23 |
22
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( 𝐺 ‘ ( 𝑓 ‘ 0 ) ) = ( 𝐺 ‘ 𝑂 ) ) |
24 |
|
iiuni |
⊢ ( 0 [,] 1 ) = ∪ II |
25 |
24 2
|
cnf |
⊢ ( 𝑓 ∈ ( II Cn 𝐾 ) → 𝑓 : ( 0 [,] 1 ) ⟶ 𝑌 ) |
26 |
17 25
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → 𝑓 : ( 0 [,] 1 ) ⟶ 𝑌 ) |
27 |
|
0elunit |
⊢ 0 ∈ ( 0 [,] 1 ) |
28 |
|
fvco3 |
⊢ ( ( 𝑓 : ( 0 [,] 1 ) ⟶ 𝑌 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐺 ∘ 𝑓 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑓 ‘ 0 ) ) ) |
29 |
26 27 28
|
sylancl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( ( 𝐺 ∘ 𝑓 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑓 ‘ 0 ) ) ) |
30 |
9
|
ad3antrrr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) ) |
31 |
23 29 30
|
3eqtr4rd |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( 𝐹 ‘ 𝑃 ) = ( ( 𝐺 ∘ 𝑓 ) ‘ 0 ) ) |
32 |
1 15 16 20 21 31
|
cvmliftiota |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ) = ( 𝐺 ∘ 𝑓 ) ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 0 ) = 𝑃 ) ) |
33 |
32
|
simp2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( 𝐹 ∘ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ) = ( 𝐺 ∘ 𝑓 ) ) |
34 |
33
|
fveq1d |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( ( 𝐹 ∘ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ) ‘ 1 ) = ( ( 𝐺 ∘ 𝑓 ) ‘ 1 ) ) |
35 |
32
|
simp1d |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ∈ ( II Cn 𝐶 ) ) |
36 |
24 1
|
cnf |
⊢ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ∈ ( II Cn 𝐶 ) → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) : ( 0 [,] 1 ) ⟶ 𝐵 ) |
37 |
35 36
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) : ( 0 [,] 1 ) ⟶ 𝐵 ) |
38 |
|
1elunit |
⊢ 1 ∈ ( 0 [,] 1 ) |
39 |
|
fvco3 |
⊢ ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) : ( 0 [,] 1 ) ⟶ 𝐵 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ) ‘ 1 ) = ( 𝐹 ‘ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) ) |
40 |
37 38 39
|
sylancl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( ( 𝐹 ∘ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ) ‘ 1 ) = ( 𝐹 ‘ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) ) |
41 |
|
fvco3 |
⊢ ( ( 𝑓 : ( 0 [,] 1 ) ⟶ 𝑌 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 𝐺 ∘ 𝑓 ) ‘ 1 ) = ( 𝐺 ‘ ( 𝑓 ‘ 1 ) ) ) |
42 |
26 38 41
|
sylancl |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( ( 𝐺 ∘ 𝑓 ) ‘ 1 ) = ( 𝐺 ‘ ( 𝑓 ‘ 1 ) ) ) |
43 |
|
simprr |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( 𝑓 ‘ 1 ) = 𝑦 ) |
44 |
43
|
fveq2d |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( 𝐺 ‘ ( 𝑓 ‘ 1 ) ) = ( 𝐺 ‘ 𝑦 ) ) |
45 |
42 44
|
eqtrd |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( ( 𝐺 ∘ 𝑓 ) ‘ 1 ) = ( 𝐺 ‘ 𝑦 ) ) |
46 |
34 40 45
|
3eqtr3d |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( 𝐹 ‘ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) = ( 𝐺 ‘ 𝑦 ) ) |
47 |
|
fveqeq2 |
⊢ ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑦 ) → ( ( 𝐹 ‘ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) = ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐹 ‘ ( 𝐻 ‘ 𝑦 ) ) = ( 𝐺 ‘ 𝑦 ) ) ) |
48 |
46 47
|
syl5ibcom |
⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ) → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑦 ) → ( 𝐹 ‘ ( 𝐻 ‘ 𝑦 ) ) = ( 𝐺 ‘ 𝑦 ) ) ) |
49 |
48
|
expimpd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) → ( ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ) ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑦 ) ) → ( 𝐹 ‘ ( 𝐻 ‘ 𝑦 ) ) = ( 𝐺 ‘ 𝑦 ) ) ) |
50 |
14 49
|
syl5bi |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑦 ) ) → ( 𝐹 ‘ ( 𝐻 ‘ 𝑦 ) ) = ( 𝐺 ‘ 𝑦 ) ) ) |
51 |
50
|
rexlimdva |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑦 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( 𝐻 ‘ 𝑦 ) ) → ( 𝐹 ‘ ( 𝐻 ‘ 𝑦 ) ) = ( 𝐺 ‘ 𝑦 ) ) ) |
52 |
13 51
|
mpd |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐹 ‘ ( 𝐻 ‘ 𝑦 ) ) = ( 𝐺 ‘ 𝑦 ) ) |
53 |
52
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑦 ∈ 𝑌 ↦ ( 𝐹 ‘ ( 𝐻 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝐺 ‘ 𝑦 ) ) ) |
54 |
1 2 3 4 5 6 7 8 9 10
|
cvmlift3lem3 |
⊢ ( 𝜑 → 𝐻 : 𝑌 ⟶ 𝐵 ) |
55 |
54
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 ) |
56 |
54
|
feqmptd |
⊢ ( 𝜑 → 𝐻 = ( 𝑦 ∈ 𝑌 ↦ ( 𝐻 ‘ 𝑦 ) ) ) |
57 |
|
cvmcn |
⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) ) |
58 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
59 |
1 58
|
cnf |
⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 ) |
60 |
3 57 59
|
3syl |
⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ∪ 𝐽 ) |
61 |
60
|
feqmptd |
⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ 𝐵 ↦ ( 𝐹 ‘ 𝑤 ) ) ) |
62 |
|
fveq2 |
⊢ ( 𝑤 = ( 𝐻 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑦 ) ) ) |
63 |
55 56 61 62
|
fmptco |
⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝐹 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) |
64 |
2 58
|
cnf |
⊢ ( 𝐺 ∈ ( 𝐾 Cn 𝐽 ) → 𝐺 : 𝑌 ⟶ ∪ 𝐽 ) |
65 |
7 64
|
syl |
⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ∪ 𝐽 ) |
66 |
65
|
feqmptd |
⊢ ( 𝜑 → 𝐺 = ( 𝑦 ∈ 𝑌 ↦ ( 𝐺 ‘ 𝑦 ) ) ) |
67 |
53 63 66
|
3eqtr4d |
⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) = 𝐺 ) |