Metamath Proof Explorer

Theorem cvmlift3lem2

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 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
Assertion cvmlift3lem2 ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ∃! 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )

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 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → 𝐾 ∈ SConn )
11 sconnpconn ⊢ ( 𝐾 ∈ SConn → 𝐾 ∈ PConn )
12 10 11 syl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → 𝐾 ∈ PConn )
13 6 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → 𝑂 ∈ 𝑌 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → 𝑋 ∈ 𝑌 )
15 2 pconncn ⊢ ( ( 𝐾 ∈ PConn ∧ 𝑂 ∈ 𝑌 ∧ 𝑋 ∈ 𝑌 ) → ∃ 𝑎 ∈ ( II Cn 𝐾 ) ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) )
16 12 13 14 15 syl3anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ∃ 𝑎 ∈ ( II Cn 𝐾 ) ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) )
17 eqid ⊢ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
18 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
19 simprl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → 𝑎 ∈ ( II Cn 𝐾 ) )
20 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
21 cnco ⊢ ( ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝐺 ∘ 𝑎 ) ∈ ( II Cn 𝐽 ) )
22 19 20 21 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( 𝐺 ∘ 𝑎 ) ∈ ( II Cn 𝐽 ) )
23 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → 𝑃 ∈ 𝐵 )
24 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( 𝑎 ‘ 0 ) = 𝑂 )
25 24 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( 𝐺 ‘ ( 𝑎 ‘ 0 ) ) = ( 𝐺 ‘ 𝑂 ) )
26 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
27 26 2 cnf ⊢ ( 𝑎 ∈ ( II Cn 𝐾 ) → 𝑎 : ( 0 [,] 1 ) ⟶ 𝑌 )
28 19 27 syl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → 𝑎 : ( 0 [,] 1 ) ⟶ 𝑌 )
29 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
30 fvco3 ⊢ ( ( 𝑎 : ( 0 [,] 1 ) ⟶ 𝑌 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐺 ∘ 𝑎 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑎 ‘ 0 ) ) )
31 28 29 30 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( ( 𝐺 ∘ 𝑎 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑎 ‘ 0 ) ) )
32 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
33 25 31 32 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( ( 𝐺 ∘ 𝑎 ) ‘ 0 ) )
34 1 17 18 22 23 33 cvmliftiota ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ) = ( 𝐺 ∘ 𝑎 ) ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 0 ) = 𝑃 ) )
35 34 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ∈ ( II Cn 𝐶 ) )
36 26 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 ffvelcdm ⊢ ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) : ( 0 [,] 1 ) ⟶ 𝐵 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ∈ 𝐵 )
40 37 38 39 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ∈ 𝐵 )
41 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( 𝑎 ‘ 1 ) = 𝑋 )
42 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) )
43 fveq1 ⊢ ( 𝑓 = 𝑎 → ( 𝑓 ‘ 0 ) = ( 𝑎 ‘ 0 ) )
44 43 eqeq1d ⊢ ( 𝑓 = 𝑎 → ( ( 𝑓 ‘ 0 ) = 𝑂 ↔ ( 𝑎 ‘ 0 ) = 𝑂 ) )
45 fveq1 ⊢ ( 𝑓 = 𝑎 → ( 𝑓 ‘ 1 ) = ( 𝑎 ‘ 1 ) )
46 45 eqeq1d ⊢ ( 𝑓 = 𝑎 → ( ( 𝑓 ‘ 1 ) = 𝑋 ↔ ( 𝑎 ‘ 1 ) = 𝑋 ) )
47 coeq2 ⊢ ( 𝑓 = 𝑎 → ( 𝐺 ∘ 𝑓 ) = ( 𝐺 ∘ 𝑎 ) )
48 47 eqeq2d ⊢ ( 𝑓 = 𝑎 → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ) )
49 48 anbi1d ⊢ ( 𝑓 = 𝑎 → ( ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
50 49 riotabidv ⊢ ( 𝑓 = 𝑎 → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
51 50 fveq1d ⊢ ( 𝑓 = 𝑎 → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) )
52 51 eqeq1d ⊢ ( 𝑓 = 𝑎 → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ↔ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) )
53 44 46 52 3anbi123d ⊢ ( 𝑓 = 𝑎 → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) ↔ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) ) )
54 53 rspcev ⊢ ( ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) )
55 19 24 41 42 54 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) )
56 3 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
57 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → 𝐾 ∈ SConn )
58 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → 𝐾 ∈ 𝑛-Locally PConn )
59 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → 𝑂 ∈ 𝑌 )
60 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
61 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → 𝑃 ∈ 𝐵 )
62 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
63 19 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → 𝑎 ∈ ( II Cn 𝐾 ) )
64 24 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ( 𝑎 ‘ 0 ) = 𝑂 )
65 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ℎ ∈ ( II Cn 𝐾 ) )
66 simprr1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ( ℎ ‘ 0 ) = 𝑂 )
67 41 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ( 𝑎 ‘ 1 ) = 𝑋 )
68 simprr2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ( ℎ ‘ 1 ) = 𝑋 )
69 67 68 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ( 𝑎 ‘ 1 ) = ( ℎ ‘ 1 ) )
70 1 2 56 57 58 59 60 61 62 63 64 65 66 69 cvmlift3lem1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) )
71 simprr3 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 )
72 70 71 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) ∧ ( ℎ ∈ ( II Cn 𝐾 ) ∧ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 )
73 72 rexlimdvaa ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) ∧ 𝑤 ∈ 𝐵 ) → ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) )
74 73 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ∀ 𝑤 ∈ 𝐵 ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) )
75 eqeq2 ⊢ ( 𝑧 = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ↔ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) )
76 75 3anbi3d ⊢ ( 𝑧 = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) ) )
77 76 rexbidv ⊢ ( 𝑧 = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) ) )
78 eqeq1 ⊢ ( 𝑧 = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) → ( 𝑧 = 𝑤 ↔ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) )
79 78 imbi2d ⊢ ( 𝑧 = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) → ( ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) )
80 79 ralbidv ⊢ ( 𝑧 = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) → ( ∀ 𝑤 ∈ 𝐵 ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → 𝑧 = 𝑤 ) ↔ ∀ 𝑤 ∈ 𝐵 ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) )
81 77 80 anbi12d ⊢ ( 𝑧 = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) → ( ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → 𝑧 = 𝑤 ) ) ↔ ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) )
82 81 rspcev ⊢ ( ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ∈ 𝐵 ∧ ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑎 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) ) → ∃ 𝑧 ∈ 𝐵 ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → 𝑧 = 𝑤 ) ) )
83 40 55 74 82 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ∃ 𝑧 ∈ 𝐵 ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → 𝑧 = 𝑤 ) ) )
84 fveq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 ‘ 0 ) = ( ℎ ‘ 0 ) )
85 84 eqeq1d ⊢ ( 𝑓 = ℎ → ( ( 𝑓 ‘ 0 ) = 𝑂 ↔ ( ℎ ‘ 0 ) = 𝑂 ) )
86 fveq1 ⊢ ( 𝑓 = ℎ → ( 𝑓 ‘ 1 ) = ( ℎ ‘ 1 ) )
87 86 eqeq1d ⊢ ( 𝑓 = ℎ → ( ( 𝑓 ‘ 1 ) = 𝑋 ↔ ( ℎ ‘ 1 ) = 𝑋 ) )
88 coeq2 ⊢ ( 𝑓 = ℎ → ( 𝐺 ∘ 𝑓 ) = ( 𝐺 ∘ ℎ ) )
89 88 eqeq2d ⊢ ( 𝑓 = ℎ → ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ) )
90 89 anbi1d ⊢ ( 𝑓 = ℎ → ( ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
91 90 riotabidv ⊢ ( 𝑓 = ℎ → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
92 91 fveq1d ⊢ ( 𝑓 = ℎ → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) )
93 92 eqeq1d ⊢ ( 𝑓 = ℎ → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ↔ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )
94 85 87 93 3anbi123d ⊢ ( 𝑓 = ℎ → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
95 94 cbvrexvw ⊢ ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )
96 eqeq2 ⊢ ( 𝑧 = 𝑤 → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ↔ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) )
97 96 3anbi3d ⊢ ( 𝑧 = 𝑤 → ( ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) )
98 97 rexbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) )
99 95 98 bitrid ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) ) )
100 99 reu8 ⊢ ( ∃! 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐵 ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐵 ( ∃ ℎ ∈ ( II Cn 𝐾 ) ( ( ℎ ‘ 0 ) = 𝑂 ∧ ( ℎ ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ ℎ ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑤 ) → 𝑧 = 𝑤 ) ) )
101 83 100 sylibr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑎 ∈ ( II Cn 𝐾 ) ∧ ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) ) ) → ∃! 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )
102 101 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( ∃ 𝑎 ∈ ( II Cn 𝐾 ) ( ( 𝑎 ‘ 0 ) = 𝑂 ∧ ( 𝑎 ‘ 1 ) = 𝑋 ) → ∃! 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
103 16 102 mpd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ∃! 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )