Metamath Proof Explorer

Theorem cvmlift3lem3

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

Ref Expression
Hypotheses cvmlift3.b ⊢ B = ⋃ C
cvmlift3.y ⊢ Y = ⋃ K
cvmlift3.f ⊢ φ → F ∈ C CovMap J
cvmlift3.k ⊢ φ → K ∈ SConn
cvmlift3.l ⊢ φ → K ∈ N-Locally PConn
cvmlift3.o ⊢ φ → O ∈ Y
cvmlift3.g ⊢ φ → G ∈ K Cn J
cvmlift3.p ⊢ φ → P ∈ B
cvmlift3.e ⊢ φ → F ⁡ P = G ⁡ O
cvmlift3.h ⊢ H = x ∈ Y ⟼ ι z ∈ B | ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = x ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = z
Assertion cvmlift3lem3 ⊢ φ → H : Y ⟶ B

Proof

Step Hyp Ref Expression
1 cvmlift3.b ⊢ B = ⋃ C
2 cvmlift3.y ⊢ Y = ⋃ K
3 cvmlift3.f ⊢ φ → F ∈ C CovMap J
4 cvmlift3.k ⊢ φ → K ∈ SConn
5 cvmlift3.l ⊢ φ → K ∈ N-Locally PConn
6 cvmlift3.o ⊢ φ → O ∈ Y
7 cvmlift3.g ⊢ φ → G ∈ K Cn J
8 cvmlift3.p ⊢ φ → P ∈ B
9 cvmlift3.e ⊢ φ → F ⁡ P = G ⁡ O
10 cvmlift3.h ⊢ H = x ∈ Y ⟼ ι z ∈ B | ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = x ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = z
11 1 2 3 4 5 6 7 8 9 cvmlift3lem2 ⊢ φ ∧ x ∈ Y → ∃! z ∈ B ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = x ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = z
12 riotacl ⊢ ∃! z ∈ B ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = x ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = z → ι z ∈ B | ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = x ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = z ∈ B
13 11 12 syl ⊢ φ ∧ x ∈ Y → ι z ∈ B | ∃ f ∈ II Cn K f ⁡ 0 = O ∧ f ⁡ 1 = x ∧ ι g ∈ II Cn C | F ∘ g = G ∘ f ∧ g ⁡ 0 = P ⁡ 1 = z ∈ B
14 13 10 fmptd ⊢ φ → H : Y ⟶ B