Metamath Proof Explorer

Theorem cvmlift3lem4

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 cvmlift3lem4 ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( ( 𝐻 ‘ 𝑋 ) = 𝐴 ↔ ∃ 𝑓 ∈ ( 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 cvmlift3.h ⊢ 𝐻 = ( 𝑥 ∈ 𝑌 ↦ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
11 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 ⊢ ( 𝜑 → 𝐻 : 𝑌 ⟶ 𝐵 )
12 11 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( 𝐻 ‘ 𝑋 ) ∈ 𝐵 )
13 eleq1 ⊢ ( ( 𝐻 ‘ 𝑋 ) = 𝐴 → ( ( 𝐻 ‘ 𝑋 ) ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
14 12 13 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( ( 𝐻 ‘ 𝑋 ) = 𝐴 → 𝐴 ∈ 𝐵 ) )
15 eqid ⊢ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
16 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
17 simprl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → 𝑓 ∈ ( II Cn 𝐾 ) )
18 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
19 cnco ⊢ ( ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ 𝐺 ∈ ( 𝐾 Cn 𝐽 ) ) → ( 𝐺 ∘ 𝑓 ) ∈ ( II Cn 𝐽 ) )
20 17 18 19 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( 𝐺 ∘ 𝑓 ) ∈ ( II Cn 𝐽 ) )
21 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → 𝑃 ∈ 𝐵 )
22 simprr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( 𝑓 ‘ 0 ) = 𝑂 )
23 22 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( 𝐺 ‘ ( 𝑓 ‘ 0 ) ) = ( 𝐺 ‘ 𝑂 ) )
24 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
25 24 2 cnf ⊢ ( 𝑓 ∈ ( II Cn 𝐾 ) → 𝑓 : ( 0 [,] 1 ) ⟶ 𝑌 )
26 17 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → 𝑓 : ( 0 [,] 1 ) ⟶ 𝑌 )
27 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
28 fvco3 ⊢ ( ( 𝑓 : ( 0 [,] 1 ) ⟶ 𝑌 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐺 ∘ 𝑓 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑓 ‘ 0 ) ) )
29 26 27 28 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( ( 𝐺 ∘ 𝑓 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑓 ‘ 0 ) ) )
30 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
31 23 29 30 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( 𝐹 ‘ 𝑃 ) = ( ( 𝐺 ∘ 𝑓 ) ‘ 0 ) )
32 1 15 16 20 21 31 cvmliftiota ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ) = ( 𝐺 ∘ 𝑓 ) ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 0 ) = 𝑃 ) )
33 32 simp1d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ∈ ( II Cn 𝐶 ) )
34 24 1 cnf ⊢ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ∈ ( II Cn 𝐶 ) → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) : ( 0 [,] 1 ) ⟶ 𝐵 )
35 33 34 syl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) : ( 0 [,] 1 ) ⟶ 𝐵 )
36 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
37 ffvelcdm ⊢ ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) : ( 0 [,] 1 ) ⟶ 𝐵 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ∈ 𝐵 )
38 35 36 37 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ∈ 𝐵 )
39 eleq1 ⊢ ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ∈ 𝐵 ↔ 𝐴 ∈ 𝐵 ) )
40 38 39 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = 𝑂 ) ) → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 → 𝐴 ∈ 𝐵 ) )
41 40 expr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) → ( ( 𝑓 ‘ 0 ) = 𝑂 → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 → 𝐴 ∈ 𝐵 ) ) )
42 41 a1dd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) → ( ( 𝑓 ‘ 0 ) = 𝑂 → ( ( 𝑓 ‘ 1 ) = 𝑋 → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 → 𝐴 ∈ 𝐵 ) ) ) )
43 42 3impd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 ) → 𝐴 ∈ 𝐵 ) )
44 43 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 ) → 𝐴 ∈ 𝐵 ) )
45 eqeq2 ⊢ ( 𝑥 = 𝑋 → ( ( 𝑓 ‘ 1 ) = 𝑥 ↔ ( 𝑓 ‘ 1 ) = 𝑋 ) )
46 45 3anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
47 46 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
48 47 riotabidv ⊢ ( 𝑥 = 𝑋 → ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) = ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
49 riotaex ⊢ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) ∈ V
50 48 10 49 fvmpt ⊢ ( 𝑋 ∈ 𝑌 → ( 𝐻 ‘ 𝑋 ) = ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
51 50 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( 𝐻 ‘ 𝑋 ) = ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
52 51 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( ( 𝐻 ‘ 𝑋 ) = 𝐴 ↔ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) = 𝐴 ) )
53 52 adantl ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ) → ( ( 𝐻 ‘ 𝑋 ) = 𝐴 ↔ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) = 𝐴 ) )
54 1 2 3 4 5 6 7 8 9 cvmlift3lem2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ∃! 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )
55 eqeq2 ⊢ ( 𝑧 = 𝐴 → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ↔ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 ) )
56 55 3anbi3d ⊢ ( 𝑧 = 𝐴 → ( ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 ) ) )
57 56 rexbidv ⊢ ( 𝑧 = 𝐴 → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 ) ) )
58 57 riota2 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∃! 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 ) ↔ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) = 𝐴 ) )
59 54 58 sylan2 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ) → ( ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 ) ↔ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) = 𝐴 ) )
60 53 59 bitr4d ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) ) → ( ( 𝐻 ‘ 𝑋 ) = 𝐴 ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 ) ) )
61 60 expcom ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( 𝐴 ∈ 𝐵 → ( ( 𝐻 ‘ 𝑋 ) = 𝐴 ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 ) ) ) )
62 14 44 61 pm5.21ndd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( ( 𝐻 ‘ 𝑋 ) = 𝐴 ↔ ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑋 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝐴 ) ) )