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
|
ffvelrnda |
⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑌 ) → ( 𝐻 ‘ 𝑋 ) ∈ 𝐵 ) |
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 |
|
ffvelrn |
⊢ ( ( ( ℩ 𝑔 ∈ ( 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 ) = 𝐴 ) ) ) |