Metamath Proof Explorer

Theorem cvmlift2lem7

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 cvmlift2lem7 ⊢ φ → F ∘ K = G

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 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
9 1 2 3 4 5 6 8 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
10 9 adantrr ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 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
11 10 simp2d ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 0 1 → F ∘ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x = z ∈ 0 1 ⟼ x G z
12 11 fveq1d ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 0 1 → F ∘ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y = z ∈ 0 1 ⟼ x G z ⁡ y
13 10 simp1d ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 0 1 → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ∈ II Cn C
14 iiuni ⊢ 0 1 = ⋃ II
15 14 1 cnf ⊢ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ∈ II Cn C → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x : 0 1 ⟶ B
16 13 15 syl ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 0 1 → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x : 0 1 ⟶ B
17 simprr ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 0 1 → y ∈ 0 1
18 fvco3 ⊢ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x : 0 1 ⟶ B ∧ y ∈ 0 1 → F ∘ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y = F ⁡ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y
19 16 17 18 syl2anc ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 0 1 → F ∘ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y = F ⁡ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y
20 oveq2 ⊢ z = y → x G z = x G y
21 eqid ⊢ z ∈ 0 1 ⟼ x G z = z ∈ 0 1 ⟼ x G z
22 ovex ⊢ x G y ∈ V
23 20 21 22 fvmpt ⊢ y ∈ 0 1 → z ∈ 0 1 ⟼ x G z ⁡ y = x G y
24 17 23 syl ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 0 1 → z ∈ 0 1 ⟼ x G z ⁡ y = x G y
25 12 19 24 3eqtr3d ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 0 1 → F ⁡ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y = x G y
26 25 3impb ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 0 1 → F ⁡ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y = x G y
27 26 mpoeq3dva ⊢ φ → x ∈ 0 1 , y ∈ 0 1 ⟼ F ⁡ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y = x ∈ 0 1 , y ∈ 0 1 ⟼ x G y
28 16 17 ffvelrnd ⊢ φ ∧ x ∈ 0 1 ∧ y ∈ 0 1 → ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y ∈ B
29 7 a1i ⊢ φ → K = x ∈ 0 1 , y ∈ 0 1 ⟼ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y
30 cvmcn ⊢ F ∈ C CovMap J → F ∈ C Cn J
31 eqid ⊢ ⋃ J = ⋃ J
32 1 31 cnf ⊢ F ∈ C Cn J → F : B ⟶ ⋃ J
33 2 30 32 3syl ⊢ φ → F : B ⟶ ⋃ J
34 33 feqmptd ⊢ φ → F = w ∈ B ⟼ F ⁡ w
35 fveq2 ⊢ w = ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y → F ⁡ w = F ⁡ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y
36 28 29 34 35 fmpoco ⊢ φ → F ∘ K = x ∈ 0 1 , y ∈ 0 1 ⟼ F ⁡ ι f ∈ II Cn C | F ∘ f = z ∈ 0 1 ⟼ x G z ∧ f ⁡ 0 = H ⁡ x ⁡ y
37 iitop ⊢ II ∈ Top
38 37 37 14 14 txunii ⊢ 0 1 × 0 1 = ⋃ II × t II
39 38 31 cnf ⊢ G ∈ II × t II Cn J → G : 0 1 × 0 1 ⟶ ⋃ J
40 ffn ⊢ G : 0 1 × 0 1 ⟶ ⋃ J → G Fn 0 1 × 0 1
41 3 39 40 3syl ⊢ φ → G Fn 0 1 × 0 1
42 fnov ⊢ G Fn 0 1 × 0 1 ↔ G = x ∈ 0 1 , y ∈ 0 1 ⟼ x G y
43 41 42 sylib ⊢ φ → G = x ∈ 0 1 , y ∈ 0 1 ⟼ x G y
44 27 36 43 3eqtr4d ⊢ φ → F ∘ K = G