Theorem cvmlift2lem3

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 ) = 𝑃 ) )
	cvmlift2lem3.1	⊢ 𝐾 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
Assertion	cvmlift2lem3	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐾 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝐾 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )

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		cvmlift2lem3.1	⊢ 𝐾 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
8	2	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
9		iitopon	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
10	9	a1i	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
11		simpr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → 𝑋 ∈ ( 0 [,] 1 ) )
12	10 10 11	cnmptc	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑋 ) ∈ ( II Cn II ) )
13	10	cnmptid	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑧 ) ∈ ( II Cn II ) )
14	3	adantr	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
15	10 12 13 14	cnmpt12f	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∈ ( II Cn 𝐽 ) )
16	1 2 3 4 5 6	cvmlift2lem2	⊢ ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐻 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) )
17	16	simp1d	⊢ ( 𝜑 → 𝐻 ∈ ( II Cn 𝐶 ) )
18		iiuni	⊢ ( 0 [,] 1 ) = ∪ II
19	18 1	cnf	⊢ ( 𝐻 ∈ ( II Cn 𝐶 ) → 𝐻 : ( 0 [,] 1 ) ⟶ 𝐵 )
20	17 19	syl	⊢ ( 𝜑 → 𝐻 : ( 0 [,] 1 ) ⟶ 𝐵 )
21	20	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐻 ‘ 𝑋 ) ∈ 𝐵 )
22		0elunit	⊢ 0 ∈ ( 0 [,] 1 )
23		oveq2	⊢ ( 𝑧 = 0 → ( 𝑋 𝐺 𝑧 ) = ( 𝑋 𝐺 0 ) )
24		eqid	⊢ ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) )
25		ovex	⊢ ( 𝑋 𝐺 0 ) ∈ V
26	23 24 25	fvmpt	⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ‘ 0 ) = ( 𝑋 𝐺 0 ) )
27	22 26	mp1i	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ‘ 0 ) = ( 𝑋 𝐺 0 ) )
28	16	simp2d	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐻 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) )
29	28	fveq1d	⊢ ( 𝜑 → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑋 ) = ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ‘ 𝑋 ) )
30		oveq1	⊢ ( 𝑧 = 𝑋 → ( 𝑧 𝐺 0 ) = ( 𝑋 𝐺 0 ) )
31		eqid	⊢ ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) )
32	30 31 25	fvmpt	⊢ ( 𝑋 ∈ ( 0 [,] 1 ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ‘ 𝑋 ) = ( 𝑋 𝐺 0 ) )
33	29 32	sylan9eq	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑋 ) = ( 𝑋 𝐺 0 ) )
34		fvco3	⊢ ( ( 𝐻 : ( 0 [,] 1 ) ⟶ 𝐵 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) )
35	20 34	sylan	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ∘ 𝐻 ) ‘ 𝑋 ) = ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) )
36	27 33 35	3eqtr2rd	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ ( 𝐻 ‘ 𝑋 ) ) = ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ‘ 0 ) )
37	1 7 8 15 21 36	cvmliftiota	⊢ ( ( 𝜑 ∧ 𝑋 ∈ ( 0 [,] 1 ) ) → ( 𝐾 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝐾 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )