Metamath Proof Explorer

Theorem cvmlift2lem6

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

Ref Expression
Hypotheses cvmlift2.b ⊢ 𝐵 = ∪ 𝐶
cvmlift2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmlift2.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
cvmlift2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmlift2.i ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
cvmlift2.h ⊢ 𝐻 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
cvmlift2.k ⊢ 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
Assertion cvmlift2lem6 ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐾 ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) Cn 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cvmlift2.b ⊢ 𝐵 = ∪ 𝐶
2 cvmlift2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
3 cvmlift2.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
4 cvmlift2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
5 cvmlift2.i ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
6 cvmlift2.h ⊢ 𝐻 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
7 cvmlift2.k ⊢ 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
8 1 2 3 4 5 6 7 cvmlift2lem5 ⊢ ( 𝜑 → 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → 𝐾 : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝐵 )
10 9 ffnd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → 𝐾 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) )
11 fnov ⊢ ( 𝐾 Fn ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ↔ 𝐾 = ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐾 𝑣 ) ) )
12 10 11 sylib ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → 𝐾 = ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐾 𝑣 ) ) )
13 12 reseq1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐾 ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) = ( ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐾 𝑣 ) ) ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → 𝑋 ∈ ( 0 [,] 1 ) )
15 14 snssd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → { 𝑋 } ⊆ ( 0 [,] 1 ) )
16 ssid ⊢ ( 0 [,] 1 ) ⊆ ( 0 [,] 1 )
17 resmpo ⊢ ( ( { 𝑋 } ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ⊆ ( 0 [,] 1 ) ) → ( ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐾 𝑣 ) ) ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) = ( 𝑢 ∈ { 𝑋 } , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐾 𝑣 ) ) )
18 15 16 17 sylancl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐾 𝑣 ) ) ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) = ( 𝑢 ∈ { 𝑋 } , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐾 𝑣 ) ) )
19 elsni ⊢ ( 𝑢 ∈ { 𝑋 } → 𝑢 = 𝑋 )
20 19 3ad2ant2 ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) ∧ 𝑢 ∈ { 𝑋 } ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑢 = 𝑋 )
21 20 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) ∧ 𝑢 ∈ { 𝑋 } ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑢 𝐾 𝑣 ) = ( 𝑋 𝐾 𝑣 ) )
22 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) ∧ 𝑢 ∈ { 𝑋 } ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑋 ∈ ( 0 [,] 1 ) )
23 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) ∧ 𝑢 ∈ { 𝑋 } ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → 𝑣 ∈ ( 0 [,] 1 ) )
24 1 2 3 4 5 6 7 cvmlift2lem4 ⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑋 𝐾 𝑣 ) = ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑣 ) )
25 22 23 24 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) ∧ 𝑢 ∈ { 𝑋 } ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑋 𝐾 𝑣 ) = ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑣 ) )
26 21 25 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) ∧ 𝑢 ∈ { 𝑋 } ∧ 𝑣 ∈ ( 0 [,] 1 ) ) → ( 𝑢 𝐾 𝑣 ) = ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑣 ) )
27 26 mpoeq3dva ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑢 ∈ { 𝑋 } , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐾 𝑣 ) ) = ( 𝑢 ∈ { 𝑋 } , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑣 ) ) )
28 18 27 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐾 𝑣 ) ) ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) = ( 𝑢 ∈ { 𝑋 } , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑣 ) ) )
29 13 28 eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐾 ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) = ( 𝑢 ∈ { 𝑋 } , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑣 ) ) )
30 eqid ⊢ ( II ↾t { 𝑋 } ) = ( II ↾t { 𝑋 } )
31 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
32 31 a1i ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
33 eqid ⊢ ( II ↾t ( 0 [,] 1 ) ) = ( II ↾t ( 0 [,] 1 ) )
34 16 a1i ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 0 [,] 1 ) ⊆ ( 0 [,] 1 ) )
35 32 32 cnmpt2nd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ 𝑣 ) ∈ ( ( II ×t II ) Cn II ) )
36 eqid ⊢ ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
37 1 2 3 4 5 6 36 cvmlift2lem3 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
38 37 simp1d ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ∈ ( II Cn 𝐶 ) )
39 32 32 35 38 cnmpt21f ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑣 ) ) ∈ ( ( II ×t II ) Cn 𝐶 ) )
40 30 32 15 33 32 34 39 cnmpt2res ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑢 ∈ { 𝑋 } , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑣 ) ) ∈ ( ( ( II ↾t { 𝑋 } ) ×t ( II ↾t ( 0 [,] 1 ) ) ) Cn 𝐶 ) )
41 iitop ⊢ II ∈ Top
42 snex ⊢ { 𝑋 } ∈ V
43 ovex ⊢ ( 0 [,] 1 ) ∈ V
44 txrest ⊢ ( ( ( II ∈ Top ∧ II ∈ Top ) ∧ ( { 𝑋 } ∈ V ∧ ( 0 [,] 1 ) ∈ V ) ) → ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) = ( ( II ↾t { 𝑋 } ) ×t ( II ↾t ( 0 [,] 1 ) ) ) )
45 41 41 42 43 44 mp4an ⊢ ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) = ( ( II ↾t { 𝑋 } ) ×t ( II ↾t ( 0 [,] 1 ) ) )
46 45 oveq1i ⊢ ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) Cn 𝐶 ) = ( ( ( II ↾t { 𝑋 } ) ×t ( II ↾t ( 0 [,] 1 ) ) ) Cn 𝐶 )
47 40 46 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑢 ∈ { 𝑋 } , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑣 ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) Cn 𝐶 ) )
48 29 47 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐾 ↾ ( { 𝑋 } × ( 0 [,] 1 ) ) ) ∈ ( ( ( II ×t II ) ↾t ( { 𝑋 } × ( 0 [,] 1 ) ) ) Cn 𝐶 ) )