Metamath Proof Explorer

Theorem cvmlift2lem3

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmlift2.b ⊢ B = ⋃ C
cvmlift2.f ⊢ φ → F ∈ C CovMap J
cvmlift2.g ⊢ φ → G ∈ II × t II Cn J
cvmlift2.p ⊢ φ → P ∈ B
cvmlift2.i ⊢ φ → F ⁡ P = 0 G 0
cvmlift2.h ⊢ H = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ z G 0 ∧ f ⁡ 0 = P
cvmlift2lem3.1 ⊢ K = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X
Assertion cvmlift2lem3 ⊢ φ ∧ X ∈ 0 1 → K ∈ II Cn C ∧ F ∘ K = z ∈ 0 1 ⟼ X G z ∧ K ⁡ 0 = H ⁡ X

Proof

Step Hyp Ref Expression
1 cvmlift2.b ⊢ B = ⋃ C
2 cvmlift2.f ⊢ φ → F ∈ C CovMap J
3 cvmlift2.g ⊢ φ → G ∈ II × t II Cn J
4 cvmlift2.p ⊢ φ → P ∈ B
5 cvmlift2.i ⊢ φ → F ⁡ P = 0 G 0
6 cvmlift2.h ⊢ H = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ z G 0 ∧ f ⁡ 0 = P
7 cvmlift2lem3.1 ⊢ K = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X
8 2 adantr ⊢ φ ∧ X ∈ 0 1 → F ∈ C CovMap J
9 iitopon ⊢ II ∈ TopOn ⁡ 0 1
10 9 a1i ⊢ φ ∧ X ∈ 0 1 → II ∈ TopOn ⁡ 0 1
11 simpr ⊢ φ ∧ X ∈ 0 1 → X ∈ 0 1
12 10 10 11 cnmptc ⊢ φ ∧ X ∈ 0 1 → z ∈ 0 1 ⟼ X ∈ II Cn II
13 10 cnmptid ⊢ φ ∧ X ∈ 0 1 → z ∈ 0 1 ⟼ z ∈ II Cn II
14 3 adantr ⊢ φ ∧ X ∈ 0 1 → G ∈ II × t II Cn J
15 10 12 13 14 cnmpt12f ⊢ φ ∧ X ∈ 0 1 → z ∈ 0 1 ⟼ X G z ∈ II Cn J
16 1 2 3 4 5 6 cvmlift2lem2 ⊢ φ → H ∈ II Cn C ∧ F ∘ H = z ∈ 0 1 ⟼ z G 0 ∧ H ⁡ 0 = P
17 16 simp1d ⊢ φ → H ∈ II Cn C
18 iiuni ⊢ 0 1 = ⋃ II
19 18 1 cnf ⊢ H ∈ II Cn C → H : 0 1 ⟶ B
20 17 19 syl ⊢ φ → H : 0 1 ⟶ B
21 20 ffvelcdmda ⊢ φ ∧ X ∈ 0 1 → H ⁡ X ∈ B
22 0elunit ⊢ 0 ∈ 0 1
23 oveq2 ⊢ z = 0 → X G z = X G 0
24 eqid ⊢ z ∈ 0 1 ⟼ X G z = z ∈ 0 1 ⟼ X G z
25 ovex ⊢ X G 0 ∈ V
26 23 24 25 fvmpt ⊢ 0 ∈ 0 1 → z ∈ 0 1 ⟼ X G z ⁡ 0 = X G 0
27 22 26 mp1i ⊢ φ ∧ X ∈ 0 1 → z ∈ 0 1 ⟼ X G z ⁡ 0 = X G 0
28 16 simp2d ⊢ φ → F ∘ H = z ∈ 0 1 ⟼ z G 0
29 28 fveq1d ⊢ φ → F ∘ H ⁡ X = z ∈ 0 1 ⟼ z G 0 ⁡ X
30 oveq1 ⊢ z = X → z G 0 = X G 0
31 eqid ⊢ z ∈ 0 1 ⟼ z G 0 = z ∈ 0 1 ⟼ z G 0
32 30 31 25 fvmpt ⊢ X ∈ 0 1 → z ∈ 0 1 ⟼ z G 0 ⁡ X = X G 0
33 29 32 sylan9eq ⊢ φ ∧ X ∈ 0 1 → F ∘ H ⁡ X = X G 0
34 fvco3 ⊢ H : 0 1 ⟶ B ∧ X ∈ 0 1 → F ∘ H ⁡ X = F ⁡ H ⁡ X
35 20 34 sylan ⊢ φ ∧ X ∈ 0 1 → F ∘ H ⁡ X = F ⁡ H ⁡ X
36 27 33 35 3eqtr2rd ⊢ φ ∧ X ∈ 0 1 → F ⁡ H ⁡ X = z ∈ 0 1 ⟼ X G z ⁡ 0
37 1 7 8 15 21 36 cvmliftiota ⊢ φ ∧ X ∈ 0 1 → K ∈ II Cn C ∧ F ∘ K = z ∈ 0 1 ⟼ X G z ∧ K ⁡ 0 = H ⁡ X