Theorem cvmlift2lem2

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 ) = 𝑃 ) )
Assertion	cvmlift2lem2	⊢ ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐻 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝐻 ‘ 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		iitopon	⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
8	7	a1i	⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
9	8	cnmptid	⊢ ( 𝜑 → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ 𝑧 ) ∈ ( II Cn II ) )
10		0elunit	⊢ 0 ∈ ( 0 [,] 1 )
11	10	a1i	⊢ ( 𝜑 → 0 ∈ ( 0 [,] 1 ) )
12	8 8 11	cnmptc	⊢ ( 𝜑 → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ 0 ) ∈ ( II Cn II ) )
13	8 9 12 3	cnmpt12f	⊢ ( 𝜑 → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∈ ( II Cn 𝐽 ) )
14		oveq1	⊢ ( 𝑧 = 0 → ( 𝑧 𝐺 0 ) = ( 0 𝐺 0 ) )
15		eqid	⊢ ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) )
16		ovex	⊢ ( 0 𝐺 0 ) ∈ V
17	14 15 16	fvmpt	⊢ ( 0 ∈ ( 0 [,] 1 ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ‘ 0 ) = ( 0 𝐺 0 ) )
18	10 17	ax-mp	⊢ ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ‘ 0 ) = ( 0 𝐺 0 )
19	5 18	eqtr4di	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ‘ 0 ) )
20	1 6 2 13 4 19	cvmliftiota	⊢ ( 𝜑 → ( 𝐻 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐻 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝐻 ‘ 0 ) = 𝑃 ) )