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∈CCovMapJ
cvmlift2.g ⊢φ→G∈II×tIICnJ
cvmlift2.p ⊢φ→P∈B
cvmlift2.i ⊢φ→F⁡P=0G0
cvmlift2.h ⊢H=ιf∈IICnC|F∘f=z∈01⟼zG0∧f⁡0=P
cvmlift2.k ⊢K=x∈01,y∈01⟼ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y
Assertion cvmlift2lem13 ⊢φ→∃!g∈II×tIICnCF∘g=G∧0g0=P

Proof

Step Hyp Ref Expression
1 cvmlift2.b ⊢B=⋃C
2 cvmlift2.f ⊢φ→F∈CCovMapJ
3 cvmlift2.g ⊢φ→G∈II×tIICnJ
4 cvmlift2.p ⊢φ→P∈B
5 cvmlift2.i ⊢φ→F⁡P=0G0
6 cvmlift2.h ⊢H=ιf∈IICnC|F∘f=z∈01⟼zG0∧f⁡0=P
7 cvmlift2.k ⊢K=x∈01,y∈01⟼ιf∈IICnC|F∘f=z∈01⟼xGz∧f⁡0=H⁡x⁡y
8 fveq2 ⊢a=z→II×tIICnPC⁡a=II×tIICnPC⁡z
9 8 eleq2d ⊢a=z→K∈II×tIICnPC⁡a↔K∈II×tIICnPC⁡z
10 9 cbvrabv ⊢a∈01×01|K∈II×tIICnPC⁡a=z∈01×01|K∈II×tIICnPC⁡z
11 sneq ⊢z=b→z=b
12 11 xpeq2d ⊢z=b→01×z=01×b
13 12 sseq1d ⊢z=b→01×z⊆a∈01×01|K∈II×tIICnPC⁡a↔01×b⊆a∈01×01|K∈II×tIICnPC⁡a
14 13 cbvrabv ⊢z∈01|01×z⊆a∈01×01|K∈II×tIICnPC⁡a=b∈01|01×b⊆a∈01×01|K∈II×tIICnPC⁡a
15 simpr ⊢c=r∧d=t→d=t
16 15 eleq1d ⊢c=r∧d=t→d∈01↔t∈01
17 xpeq1 ⊢v=u→v×b=u×b
18 17 sseq1d ⊢v=u→v×b⊆a∈01×01|K∈II×tIICnPC⁡a↔u×b⊆a∈01×01|K∈II×tIICnPC⁡a
19 xpeq1 ⊢v=u→v×d=u×d
20 19 sseq1d ⊢v=u→v×d⊆a∈01×01|K∈II×tIICnPC⁡a↔u×d⊆a∈01×01|K∈II×tIICnPC⁡a
21 18 20 bibi12d ⊢v=u→v×b⊆a∈01×01|K∈II×tIICnPC⁡a↔v×d⊆a∈01×01|K∈II×tIICnPC⁡a↔u×b⊆a∈01×01|K∈II×tIICnPC⁡a↔u×d⊆a∈01×01|K∈II×tIICnPC⁡a
22 21 cbvrexvw ⊢∃v∈nei⁡II⁡cv×b⊆a∈01×01|K∈II×tIICnPC⁡a↔v×d⊆a∈01×01|K∈II×tIICnPC⁡a↔∃u∈nei⁡II⁡cu×b⊆a∈01×01|K∈II×tIICnPC⁡a↔u×d⊆a∈01×01|K∈II×tIICnPC⁡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∈01×01|K∈II×tIICnPC⁡a↔u×t⊆a∈01×01|K∈II×tIICnPC⁡a
29 28 bibi2d ⊢c=r∧d=t→u×b⊆a∈01×01|K∈II×tIICnPC⁡a↔u×d⊆a∈01×01|K∈II×tIICnPC⁡a↔u×b⊆a∈01×01|K∈II×tIICnPC⁡a↔u×t⊆a∈01×01|K∈II×tIICnPC⁡a
30 25 29 rexeqbidv ⊢c=r∧d=t→∃u∈nei⁡II⁡cu×b⊆a∈01×01|K∈II×tIICnPC⁡a↔u×d⊆a∈01×01|K∈II×tIICnPC⁡a↔∃u∈nei⁡II⁡ru×b⊆a∈01×01|K∈II×tIICnPC⁡a↔u×t⊆a∈01×01|K∈II×tIICnPC⁡a
31 22 30 bitrid ⊢c=r∧d=t→∃v∈nei⁡II⁡cv×b⊆a∈01×01|K∈II×tIICnPC⁡a↔v×d⊆a∈01×01|K∈II×tIICnPC⁡a↔∃u∈nei⁡II⁡ru×b⊆a∈01×01|K∈II×tIICnPC⁡a↔u×t⊆a∈01×01|K∈II×tIICnPC⁡a
32 16 31 anbi12d ⊢c=r∧d=t→d∈01∧∃v∈nei⁡II⁡cv×b⊆a∈01×01|K∈II×tIICnPC⁡a↔v×d⊆a∈01×01|K∈II×tIICnPC⁡a↔t∈01∧∃u∈nei⁡II⁡ru×b⊆a∈01×01|K∈II×tIICnPC⁡a↔u×t⊆a∈01×01|K∈II×tIICnPC⁡a
33 32 cbvopabv ⊢cd|d∈01∧∃v∈nei⁡II⁡cv×b⊆a∈01×01|K∈II×tIICnPC⁡a↔v×d⊆a∈01×01|K∈II×tIICnPC⁡a=rt|t∈01∧∃u∈nei⁡II⁡ru×b⊆a∈01×01|K∈II×tIICnPC⁡a↔u×t⊆a∈01×01|K∈II×tIICnPC⁡a
34 1 2 3 4 5 6 7 10 14 33 cvmlift2lem12 ⊢φ→K∈II×tIICnC
35 1 2 3 4 5 6 7 cvmlift2lem7 ⊢φ→F∘K=G
36 0elunit ⊢0∈01
37 1 2 3 4 5 6 7 cvmlift2lem8 ⊢φ∧0∈01→0K0=H⁡0
38 36 37 mpan2 ⊢φ→0K0=H⁡0
39 1 2 3 4 5 6 cvmlift2lem2 ⊢φ→H∈IICnC∧F∘H=z∈01⟼zG0∧H⁡0=P
40 39 simp3d ⊢φ→H⁡0=P
41 38 40 eqtrd ⊢φ→0K0=P
42 coeq2 ⊢g=K→F∘g=F∘K
43 42 eqeq1d ⊢g=K→F∘g=G↔F∘K=G
44 oveq ⊢g=K→0g0=0K0
45 44 eqeq1d ⊢g=K→0g0=P↔0K0=P
46 43 45 anbi12d ⊢g=K→F∘g=G∧0g0=P↔F∘K=G∧0K0=P
47 46 rspcev ⊢K∈II×tIICnC∧F∘K=G∧0K0=P→∃g∈II×tIICnCF∘g=G∧0g0=P
48 34 35 41 47 syl12anc ⊢φ→∃g∈II×tIICnCF∘g=G∧0g0=P
49 iitop ⊢II∈Top
50 iiuni ⊢01=⋃II
51 49 49 50 50 txunii ⊢01×01=⋃II×tII
52 iiconn ⊢II∈Conn
53 txconn ⊢II∈Conn∧II∈Conn→II×tII∈Conn
54 52 52 53 mp2an ⊢II×tII∈Conn
55 54 a1i ⊢φ→II×tII∈Conn
56 iinllyconn ⊢II∈N-Locally Conn
57 txconn ⊢x∈Conn∧y∈Conn→x×ty∈Conn
58 57 txnlly ⊢II∈N-Locally Conn ∧ II∈N-Locally Conn → II×tII∈N-Locally Conn
59 56 56 58 mp2an ⊢II×tII∈N-Locally Conn
60 59 a1i ⊢φ→II×tII∈N-Locally Conn
61 opelxpi ⊢0∈01∧0∈01→00∈01×01
62 36 36 61 mp2an ⊢00∈01×01
63 62 a1i ⊢φ→00∈01×01
64 df-ov ⊢0G0=G⁡00
65 5 64 eqtrdi ⊢φ→F⁡P=G⁡00
66 1 51 2 55 60 63 3 4 65 cvmliftmo ⊢φ→∃*g∈II×tIICnCF∘g=G∧g⁡00=P
67 df-ov ⊢0g0=g⁡00
68 67 eqeq1i ⊢0g0=P↔g⁡00=P
69 68 anbi2i ⊢F∘g=G∧0g0=P↔F∘g=G∧g⁡00=P
70 69 rmobii ⊢∃*g∈II×tIICnCF∘g=G∧0g0=P↔∃*g∈II×tIICnCF∘g=G∧g⁡00=P
71 66 70 sylibr ⊢φ→∃*g∈II×tIICnCF∘g=G∧0g0=P
72 reu5 ⊢∃!g∈II×tIICnCF∘g=G∧0g0=P↔∃g∈II×tIICnCF∘g=G∧0g0=P∧∃*g∈II×tIICnCF∘g=G∧0g0=P
73 48 71 72 sylanbrc ⊢φ→∃!g∈II×tIICnCF∘g=G∧0g0=P