Metamath Proof Explorer

Theorem cvmlift2lem13

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 cvmlift2lem13 ⊢ φ → ∃! g ∈ II × t II Cn C F ∘ g = G ∧ 0 g 0 = P

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 fveq2 ⊢ a = z → II × t II CnP C ⁡ a = II × t II CnP C ⁡ z
9 8 eleq2d ⊢ a = z → K ∈ II × t II CnP C ⁡ a ↔ K ∈ II × t II CnP C ⁡ z
10 9 cbvrabv ⊢ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a = z ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ z
11 sneq ⊢ z = b → z = b
12 11 xpeq2d ⊢ z = b → 0 1 × z = 0 1 × b
13 12 sseq1d ⊢ z = b → 0 1 × z ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ 0 1 × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
14 13 cbvrabv ⊢ z ∈ 0 1 | 0 1 × z ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a = b ∈ 0 1 | 0 1 × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
15 simpr ⊢ c = r ∧ d = t → d = t
16 15 eleq1d ⊢ c = r ∧ d = t → d ∈ 0 1 ↔ t ∈ 0 1
17 xpeq1 ⊢ v = u → v × b = u × b
18 17 sseq1d ⊢ v = u → v × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
19 xpeq1 ⊢ v = u → v × d = u × d
20 19 sseq1d ⊢ v = u → v × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
21 18 20 bibi12d ⊢ v = u → v × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ v × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
22 21 cbvrexvw ⊢ ∃ v ∈ nei ⁡ II ⁡ c v × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ v × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ ∃ u ∈ nei ⁡ II ⁡ c u × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
23 simpl ⊢ c = r ∧ d = t → c = r
24 23 sneqd ⊢ c = r ∧ d = t → c = r
25 24 fveq2d ⊢ c = r ∧ d = t → nei ⁡ II ⁡ c = nei ⁡ II ⁡ r
26 15 sneqd ⊢ c = r ∧ d = t → d = t
27 26 xpeq2d ⊢ c = r ∧ d = t → u × d = u × t
28 27 sseq1d ⊢ c = r ∧ d = t → u × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × t ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
29 28 bibi2d ⊢ c = r ∧ d = t → u × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × t ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
30 25 29 rexeqbidv ⊢ c = r ∧ d = t → ∃ u ∈ nei ⁡ II ⁡ c u × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ ∃ u ∈ nei ⁡ II ⁡ r u × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × t ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
31 22 30 syl5bb ⊢ c = r ∧ d = t → ∃ v ∈ nei ⁡ II ⁡ c v × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ v × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ ∃ u ∈ nei ⁡ II ⁡ r u × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × t ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
32 16 31 anbi12d ⊢ c = r ∧ d = t → d ∈ 0 1 ∧ ∃ v ∈ nei ⁡ II ⁡ c v × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ v × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ t ∈ 0 1 ∧ ∃ u ∈ nei ⁡ II ⁡ r u × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × t ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
33 32 cbvopabv ⊢ c d | d ∈ 0 1 ∧ ∃ v ∈ nei ⁡ II ⁡ c v × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ v × d ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a = r t | t ∈ 0 1 ∧ ∃ u ∈ nei ⁡ II ⁡ r u × b ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a ↔ u × t ⊆ a ∈ 0 1 × 0 1 | K ∈ II × t II CnP C ⁡ a
34 1 2 3 4 5 6 7 10 14 33 cvmlift2lem12 ⊢ φ → K ∈ II × t II Cn C
35 1 2 3 4 5 6 7 cvmlift2lem7 ⊢ φ → F ∘ K = G
36 0elunit ⊢ 0 ∈ 0 1
37 1 2 3 4 5 6 7 cvmlift2lem8 ⊢ φ ∧ 0 ∈ 0 1 → 0 K 0 = H ⁡ 0
38 36 37 mpan2 ⊢ φ → 0 K 0 = H ⁡ 0
39 1 2 3 4 5 6 cvmlift2lem2 ⊢ φ → H ∈ II Cn C ∧ F ∘ H = z ∈ 0 1 ⟼ z G 0 ∧ H ⁡ 0 = P
40 39 simp3d ⊢ φ → H ⁡ 0 = P
41 38 40 eqtrd ⊢ φ → 0 K 0 = P
42 coeq2 ⊢ g = K → F ∘ g = F ∘ K
43 42 eqeq1d ⊢ g = K → F ∘ g = G ↔ F ∘ K = G
44 oveq ⊢ g = K → 0 g 0 = 0 K 0
45 44 eqeq1d ⊢ g = K → 0 g 0 = P ↔ 0 K 0 = P
46 43 45 anbi12d ⊢ g = K → F ∘ g = G ∧ 0 g 0 = P ↔ F ∘ K = G ∧ 0 K 0 = P
47 46 rspcev ⊢ K ∈ II × t II Cn C ∧ F ∘ K = G ∧ 0 K 0 = P → ∃ g ∈ II × t II Cn C F ∘ g = G ∧ 0 g 0 = P
48 34 35 41 47 syl12anc ⊢ φ → ∃ g ∈ II × t II Cn C F ∘ g = G ∧ 0 g 0 = P
49 iitop ⊢ II ∈ Top
50 iiuni ⊢ 0 1 = ⋃ II
51 49 49 50 50 txunii ⊢ 0 1 × 0 1 = ⋃ II × t II
52 iiconn ⊢ II ∈ Conn
53 txconn ⊢ II ∈ Conn ∧ II ∈ Conn → II × t II ∈ Conn
54 52 52 53 mp2an ⊢ II × t II ∈ Conn
55 54 a1i ⊢ φ → II × t II ∈ Conn
56 iinllyconn ⊢ II ∈ N-Locally Conn
57 txconn ⊢ x ∈ Conn ∧ y ∈ Conn → x × t y ∈ Conn
58 57 txnlly ⊢ II ∈ N-Locally Conn ∧ II ∈ N-Locally Conn → II × t II ∈ N-Locally Conn
59 56 56 58 mp2an ⊢ II × t II ∈ N-Locally Conn
60 59 a1i ⊢ φ → II × t II ∈ N-Locally Conn
61 opelxpi ⊢ 0 ∈ 0 1 ∧ 0 ∈ 0 1 → 0 0 ∈ 0 1 × 0 1
62 36 36 61 mp2an ⊢ 0 0 ∈ 0 1 × 0 1
63 62 a1i ⊢ φ → 0 0 ∈ 0 1 × 0 1
64 df-ov ⊢ 0 G 0 = G ⁡ 0 0
65 5 64 eqtrdi ⊢ φ → F ⁡ P = G ⁡ 0 0
66 1 51 2 55 60 63 3 4 65 cvmliftmo ⊢ φ → ∃* g ∈ II × t II Cn C F ∘ g = G ∧ g ⁡ 0 0 = P
67 df-ov ⊢ 0 g 0 = g ⁡ 0 0
68 67 eqeq1i ⊢ 0 g 0 = P ↔ g ⁡ 0 0 = P
69 68 anbi2i ⊢ F ∘ g = G ∧ 0 g 0 = P ↔ F ∘ g = G ∧ g ⁡ 0 0 = P
70 69 rmobii ⊢ ∃* g ∈ II × t II Cn C F ∘ g = G ∧ 0 g 0 = P ↔ ∃* g ∈ II × t II Cn C F ∘ g = G ∧ g ⁡ 0 0 = P
71 66 70 sylibr ⊢ φ → ∃* g ∈ II × t II Cn C F ∘ g = G ∧ 0 g 0 = P
72 reu5 ⊢ ∃! g ∈ II × t II Cn C F ∘ g = G ∧ 0 g 0 = P ↔ ∃ g ∈ II × t II Cn C F ∘ g = G ∧ 0 g 0 = P ∧ ∃* g ∈ II × t II Cn C F ∘ g = G ∧ 0 g 0 = P
73 48 71 72 sylanbrc ⊢ φ → ∃! g ∈ II × t II Cn C F ∘ g = G ∧ 0 g 0 = P