Metamath Proof Explorer

Theorem cvmlift3lem9

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-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 ) = 𝑧 ) ) )
cvmlift3lem7.s ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
Assertion cvmlift3lem9 ( 𝜑 → ∃ 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) )

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 cvmlift3lem7.s ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑠 ( ∀ 𝑑 ∈ ( 𝑠 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
12 1 2 3 4 5 6 7 8 9 10 11 cvmlift3lem8 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐾 Cn 𝐶 ) )
13 1 2 3 4 5 6 7 8 9 10 cvmlift3lem5 ⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) = 𝐺 )
14 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
15 14 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
16 sconntop ⊢ ( 𝐾 ∈ SConn → 𝐾 ∈ Top )
17 4 16 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
18 2 toptopon ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
19 17 18 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
20 cnconst2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑂 ∈ 𝑌 ) → ( ( 0 [,] 1 ) × { 𝑂 } ) ∈ ( II Cn 𝐾 ) )
21 15 19 6 20 syl3anc ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { 𝑂 } ) ∈ ( II Cn 𝐾 ) )
22 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
23 fvconst2g ⊢ ( ( 𝑂 ∈ 𝑌 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 0 ) = 𝑂 )
24 6 22 23 sylancl ⊢ ( 𝜑 → ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 0 ) = 𝑂 )
25 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
26 fvconst2g ⊢ ( ( 𝑂 ∈ 𝑌 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 1 ) = 𝑂 )
27 6 25 26 sylancl ⊢ ( 𝜑 → ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 1 ) = 𝑂 )
28 9 sneqd ⊢ ( 𝜑 → { ( 𝐹 ‘ 𝑃 ) } = { ( 𝐺 ‘ 𝑂 ) } )
29 28 xpeq2d ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 𝑃 ) } ) = ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 𝑂 ) } ) )
30 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
31 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
32 1 31 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ ∪ 𝐽 )
33 ffn ⊢ ( 𝐹 : 𝐵 ⟶ ∪ 𝐽 → 𝐹 Fn 𝐵 )
34 3 30 32 33 4syl ⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
35 fcoconst ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝑃 ∈ 𝐵 ) → ( 𝐹 ∘ ( ( 0 [,] 1 ) × { 𝑃 } ) ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 𝑃 ) } ) )
36 34 8 35 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∘ ( ( 0 [,] 1 ) × { 𝑃 } ) ) = ( ( 0 [,] 1 ) × { ( 𝐹 ‘ 𝑃 ) } ) )
37 2 31 cnf ⊢ ( 𝐺 ∈ ( 𝐾 Cn 𝐽 ) → 𝐺 : 𝑌 ⟶ ∪ 𝐽 )
38 7 37 syl ⊢ ( 𝜑 → 𝐺 : 𝑌 ⟶ ∪ 𝐽 )
39 38 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑌 )
40 fcoconst ⊢ ( ( 𝐺 Fn 𝑌 ∧ 𝑂 ∈ 𝑌 ) → ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) = ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 𝑂 ) } ) )
41 39 6 40 syl2anc ⊢ ( 𝜑 → ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) = ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 𝑂 ) } ) )
42 29 36 41 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ∘ ( ( 0 [,] 1 ) × { 𝑃 } ) ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) )
43 fvconst2g ⊢ ( ( 𝑃 ∈ 𝐵 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { 𝑃 } ) ‘ 0 ) = 𝑃 )
44 8 22 43 sylancl ⊢ ( 𝜑 → ( ( ( 0 [,] 1 ) × { 𝑃 } ) ‘ 0 ) = 𝑃 )
45 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
46 3 45 syl ⊢ ( 𝜑 → 𝐶 ∈ Top )
47 1 toptopon ⊢ ( 𝐶 ∈ Top ↔ 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
48 46 47 sylib ⊢ ( 𝜑 → 𝐶 ∈ ( TopOn ‘ 𝐵 ) )
49 cnconst2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐶 ∈ ( TopOn ‘ 𝐵 ) ∧ 𝑃 ∈ 𝐵 ) → ( ( 0 [,] 1 ) × { 𝑃 } ) ∈ ( II Cn 𝐶 ) )
50 15 48 8 49 syl3anc ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { 𝑃 } ) ∈ ( II Cn 𝐶 ) )
51 cvmtop2 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐽 ∈ Top )
52 3 51 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
53 31 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
54 52 53 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
55 38 6 ffvelcdmd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑂 ) ∈ ∪ 𝐽 )
56 cnconst2 ⊢ ( ( II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) ∧ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) ∧ ( 𝐺 ‘ 𝑂 ) ∈ ∪ 𝐽 ) → ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 𝑂 ) } ) ∈ ( II Cn 𝐽 ) )
57 15 54 55 56 syl3anc ⊢ ( 𝜑 → ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 𝑂 ) } ) ∈ ( II Cn 𝐽 ) )
58 41 57 eqeltrd ⊢ ( 𝜑 → ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∈ ( II Cn 𝐽 ) )
59 fvconst2g ⊢ ( ( ( 𝐺 ‘ 𝑂 ) ∈ ∪ 𝐽 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 𝑂 ) } ) ‘ 0 ) = ( 𝐺 ‘ 𝑂 ) )
60 55 22 59 sylancl ⊢ ( 𝜑 → ( ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 𝑂 ) } ) ‘ 0 ) = ( 𝐺 ‘ 𝑂 ) )
61 41 fveq1d ⊢ ( 𝜑 → ( ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ‘ 0 ) = ( ( ( 0 [,] 1 ) × { ( 𝐺 ‘ 𝑂 ) } ) ‘ 0 ) )
62 60 61 9 3eqtr4rd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ‘ 0 ) )
63 1 cvmlift ⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ‘ 0 ) ) ) → ∃! 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
64 3 58 8 62 63 syl22anc ⊢ ( 𝜑 → ∃! 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
65 coeq2 ⊢ ( 𝑔 = ( ( 0 [,] 1 ) × { 𝑃 } ) → ( 𝐹 ∘ 𝑔 ) = ( 𝐹 ∘ ( ( 0 [,] 1 ) × { 𝑃 } ) ) )
66 65 eqeq1d ⊢ ( 𝑔 = ( ( 0 [,] 1 ) × { 𝑃 } ) → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ↔ ( 𝐹 ∘ ( ( 0 [,] 1 ) × { 𝑃 } ) ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ) )
67 fveq1 ⊢ ( 𝑔 = ( ( 0 [,] 1 ) × { 𝑃 } ) → ( 𝑔 ‘ 0 ) = ( ( ( 0 [,] 1 ) × { 𝑃 } ) ‘ 0 ) )
68 67 eqeq1d ⊢ ( 𝑔 = ( ( 0 [,] 1 ) × { 𝑃 } ) → ( ( 𝑔 ‘ 0 ) = 𝑃 ↔ ( ( ( 0 [,] 1 ) × { 𝑃 } ) ‘ 0 ) = 𝑃 ) )
69 66 68 anbi12d ⊢ ( 𝑔 = ( ( 0 [,] 1 ) × { 𝑃 } ) → ( ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ ( ( 0 [,] 1 ) × { 𝑃 } ) ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( ( ( 0 [,] 1 ) × { 𝑃 } ) ‘ 0 ) = 𝑃 ) ) )
70 69 riota2 ⊢ ( ( ( ( 0 [,] 1 ) × { 𝑃 } ) ∈ ( II Cn 𝐶 ) ∧ ∃! 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) → ( ( ( 𝐹 ∘ ( ( 0 [,] 1 ) × { 𝑃 } ) ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( ( ( 0 [,] 1 ) × { 𝑃 } ) ‘ 0 ) = 𝑃 ) ↔ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ( 0 [,] 1 ) × { 𝑃 } ) ) )
71 50 64 70 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐹 ∘ ( ( 0 [,] 1 ) × { 𝑃 } ) ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( ( ( 0 [,] 1 ) × { 𝑃 } ) ‘ 0 ) = 𝑃 ) ↔ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ( 0 [,] 1 ) × { 𝑃 } ) ) )
72 42 44 71 mpbi2and ⊢ ( 𝜑 → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ( 0 [,] 1 ) × { 𝑃 } ) )
73 72 fveq1d ⊢ ( 𝜑 → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ( 0 [,] 1 ) × { 𝑃 } ) ‘ 1 ) )
74 fvconst2g ⊢ ( ( 𝑃 ∈ 𝐵 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { 𝑃 } ) ‘ 1 ) = 𝑃 )
75 8 25 74 sylancl ⊢ ( 𝜑 → ( ( ( 0 [,] 1 ) × { 𝑃 } ) ‘ 1 ) = 𝑃 )
76 73 75 eqtrd ⊢ ( 𝜑 → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑃 )
77 fveq1 ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( 𝑓 ‘ 0 ) = ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 0 ) )
78 77 eqeq1d ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( ( 𝑓 ‘ 0 ) = 𝑂 ↔ ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 0 ) = 𝑂 ) )
79 fveq1 ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( 𝑓 ‘ 1 ) = ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 1 ) )
80 79 eqeq1d ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( ( 𝑓 ‘ 1 ) = 𝑂 ↔ ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 1 ) = 𝑂 ) )
81 coeq2 ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( 𝐺 ∘ 𝑓 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) )
82 81 eqeq2d ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ) )
83 82 anbi1d ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
84 83 riotabidv ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
85 84 fveq1d ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) )
86 85 eqeq1d ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑃 ↔ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑃 ) )
87 78 80 86 3anbi123d ⊢ ( 𝑓 = ( ( 0 [,] 1 ) × { 𝑂 } ) → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑂 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑃 ) ↔ ( ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 0 ) = 𝑂 ∧ ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 1 ) = 𝑂 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑃 ) ) )
88 87 rspcev ⊢ ( ( ( ( 0 [,] 1 ) × { 𝑂 } ) ∈ ( II Cn 𝐾 ) ∧ ( ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 0 ) = 𝑂 ∧ ( ( ( 0 [,] 1 ) × { 𝑂 } ) ‘ 1 ) = 𝑂 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ( ( 0 [,] 1 ) × { 𝑂 } ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑃 ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑂 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑃 ) )
89 21 24 27 76 88 syl13anc ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑂 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑃 ) )
90 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 ⊢ ( ( 𝜑 ∧ 𝑂 ∈ 𝑌 ) → ( ( 𝐻 ‘ 𝑂 ) = 𝑃 ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑂 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑃 ) ) )
91 6 90 mpdan ⊢ ( 𝜑 → ( ( 𝐻 ‘ 𝑂 ) = 𝑃 ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑂 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑃 ) ) )
92 89 91 mpbird ⊢ ( 𝜑 → ( 𝐻 ‘ 𝑂 ) = 𝑃 )
93 coeq2 ⊢ ( 𝑓 = 𝐻 → ( 𝐹 ∘ 𝑓 ) = ( 𝐹 ∘ 𝐻 ) )
94 93 eqeq1d ⊢ ( 𝑓 = 𝐻 → ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ↔ ( 𝐹 ∘ 𝐻 ) = 𝐺 ) )
95 fveq1 ⊢ ( 𝑓 = 𝐻 → ( 𝑓 ‘ 𝑂 ) = ( 𝐻 ‘ 𝑂 ) )
96 95 eqeq1d ⊢ ( 𝑓 = 𝐻 → ( ( 𝑓 ‘ 𝑂 ) = 𝑃 ↔ ( 𝐻 ‘ 𝑂 ) = 𝑃 ) )
97 94 96 anbi12d ⊢ ( 𝑓 = 𝐻 → ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝐻 ) = 𝐺 ∧ ( 𝐻 ‘ 𝑂 ) = 𝑃 ) ) )
98 97 rspcev ⊢ ( ( 𝐻 ∈ ( 𝐾 Cn 𝐶 ) ∧ ( ( 𝐹 ∘ 𝐻 ) = 𝐺 ∧ ( 𝐻 ‘ 𝑂 ) = 𝑃 ) ) → ∃ 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) )
99 12 13 92 98 syl12anc ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) )