Metamath Proof Explorer


Theorem cvmlift3lem5

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 6-Jul-2015)

Ref Expression
Hypotheses cvmlift3.b 𝐵 = 𝐶
cvmlift3.y 𝑌 = 𝐾
cvmlift3.f ( 𝜑𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmlift3.k ( 𝜑𝐾 ∈ SConn )
cvmlift3.l ( 𝜑𝐾 ∈ 𝑛-Locally PConn )
cvmlift3.o ( 𝜑𝑂𝑌 )
cvmlift3.g ( 𝜑𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
cvmlift3.p ( 𝜑𝑃𝐵 )
cvmlift3.e ( 𝜑 → ( 𝐹𝑃 ) = ( 𝐺𝑂 ) )
cvmlift3.h 𝐻 = ( 𝑥𝑌 ↦ ( 𝑧𝐵𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹𝑔 ) = ( 𝐺𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
Assertion cvmlift3lem5 ( 𝜑 → ( 𝐹𝐻 ) = 𝐺 )

Proof

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 ( 𝜑 → ( 𝐹𝐻 ) = 𝐺 )