Metamath Proof Explorer

Theorem cvmlift2lem6

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
cvmlift2.k ⊢ K = x ∈ 0 1 , y ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y
Assertion cvmlift2lem6 ⊢ φ ∧ X ∈ 0 1 → K ↾ X × 0 1 ∈ II × t II ↾ 𝑡 X × 0 1 Cn C

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 cvmlift2.k ⊢ K = x ∈ 0 1 , y ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y
8 1 2 3 4 5 6 7 cvmlift2lem5 ⊢ φ → K : 0 1 × 0 1 ⟶ B
9 8 adantr ⊢ φ ∧ X ∈ 0 1 → K : 0 1 × 0 1 ⟶ B
10 9 ffnd ⊢ φ ∧ X ∈ 0 1 → K Fn 0 1 × 0 1
11 fnov ⊢ K Fn 0 1 × 0 1 ↔ K = u ∈ 0 1 , v ∈ 0 1 ⟼ u K v
12 10 11 sylib ⊢ φ ∧ X ∈ 0 1 → K = u ∈ 0 1 , v ∈ 0 1 ⟼ u K v
13 12 reseq1d ⊢ φ ∧ X ∈ 0 1 → K ↾ X × 0 1 = u ∈ 0 1 , v ∈ 0 1 ⟼ u K v ↾ X × 0 1
14 simpr ⊢ φ ∧ X ∈ 0 1 → X ∈ 0 1
15 14 snssd ⊢ φ ∧ X ∈ 0 1 → X ⊆ 0 1
16 ssid ⊢ 0 1 ⊆ 0 1
17 resmpo ⊢ X ⊆ 0 1 ∧ 0 1 ⊆ 0 1 → u ∈ 0 1 , v ∈ 0 1 ⟼ u K v ↾ X × 0 1 = u ∈ X , v ∈ 0 1 ⟼ u K v
18 15 16 17 sylancl ⊢ φ ∧ X ∈ 0 1 → u ∈ 0 1 , v ∈ 0 1 ⟼ u K v ↾ X × 0 1 = u ∈ X , v ∈ 0 1 ⟼ u K v
19 elsni ⊢ u ∈ X → u = X
20 19 3ad2ant2 ⊢ φ ∧ X ∈ 0 1 ∧ u ∈ X ∧ v ∈ 0 1 → u = X
21 20 oveq1d ⊢ φ ∧ X ∈ 0 1 ∧ u ∈ X ∧ v ∈ 0 1 → u K v = X K v
22 simp1r ⊢ φ ∧ X ∈ 0 1 ∧ u ∈ X ∧ v ∈ 0 1 → X ∈ 0 1
23 simp3 ⊢ φ ∧ X ∈ 0 1 ∧ u ∈ X ∧ v ∈ 0 1 → v ∈ 0 1
24 1 2 3 4 5 6 7 cvmlift2lem4 ⊢ X ∈ 0 1 ∧ v ∈ 0 1 → X K v = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ v
25 22 23 24 syl2anc ⊢ φ ∧ X ∈ 0 1 ∧ u ∈ X ∧ v ∈ 0 1 → X K v = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ v
26 21 25 eqtrd ⊢ φ ∧ X ∈ 0 1 ∧ u ∈ X ∧ v ∈ 0 1 → u K v = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ v
27 26 mpoeq3dva ⊢ φ ∧ X ∈ 0 1 → u ∈ X , v ∈ 0 1 ⟼ u K v = u ∈ X , v ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ v
28 18 27 eqtrd ⊢ φ ∧ X ∈ 0 1 → u ∈ 0 1 , v ∈ 0 1 ⟼ u K v ↾ X × 0 1 = u ∈ X , v ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ v
29 13 28 eqtrd ⊢ φ ∧ X ∈ 0 1 → K ↾ X × 0 1 = u ∈ X , v ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ v
30 eqid ⊢ II ↾ 𝑡 X = II ↾ 𝑡 X
31 iitopon ⊢ II ∈ TopOn ⁡ 0 1
32 31 a1i ⊢ φ ∧ X ∈ 0 1 → II ∈ TopOn ⁡ 0 1
33 eqid ⊢ II ↾ 𝑡 0 1 = II ↾ 𝑡 0 1
34 16 a1i ⊢ φ ∧ X ∈ 0 1 → 0 1 ⊆ 0 1
35 32 32 cnmpt2nd ⊢ φ ∧ X ∈ 0 1 → u ∈ 0 1 , v ∈ 0 1 ⟼ v ∈ II × t II Cn II
36 eqid ⊢ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X
37 1 2 3 4 5 6 36 cvmlift2lem3 ⊢ φ ∧ X ∈ 0 1 → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ∈ II Cn C ∧ F ∘ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X = z ∈ 0 1 ⟼ X G z ∧ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ 0 = H ⁡ X
38 37 simp1d ⊢ φ ∧ X ∈ 0 1 → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ∈ II Cn C
39 32 32 35 38 cnmpt21f ⊢ φ ∧ X ∈ 0 1 → u ∈ 0 1 , v ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ v ∈ II × t II Cn C
40 30 32 15 33 32 34 39 cnmpt2res ⊢ φ ∧ X ∈ 0 1 → u ∈ X , v ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ v ∈ II ↾ 𝑡 X × t II ↾ 𝑡 0 1 Cn C
41 iitop ⊢ II ∈ Top
42 snex ⊢ X ∈ V
43 ovex ⊢ 0 1 ∈ V
44 txrest ⊢ II ∈ Top ∧ II ∈ Top ∧ X ∈ V ∧ 0 1 ∈ V → II × t II ↾ 𝑡 X × 0 1 = II ↾ 𝑡 X × t II ↾ 𝑡 0 1
45 41 41 42 43 44 mp4an ⊢ II × t II ↾ 𝑡 X × 0 1 = II ↾ 𝑡 X × t II ↾ 𝑡 0 1
46 45 oveq1i ⊢ II × t II ↾ 𝑡 X × 0 1 Cn C = II ↾ 𝑡 X × t II ↾ 𝑡 0 1 Cn C
47 40 46 eleqtrrdi ⊢ φ ∧ X ∈ 0 1 → u ∈ X , v ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ X G z ∧ f ⁡ 0 = H ⁡ X ⁡ v ∈ II × t II ↾ 𝑡 X × 0 1 Cn C
48 29 47 eqeltrd ⊢ φ ∧ X ∈ 0 1 → K ↾ X × 0 1 ∈ II × t II ↾ 𝑡 X × 0 1 Cn C