Metamath Proof Explorer

Theorem cvmlift2lem4

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 1-Jun-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	cvmlift2lem4	⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 ∈ ( 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		cvmlift2.k	⊢ 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
8		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐺 𝑧 ) = ( 𝑋 𝐺 𝑧 ) )
9	8	mpteq2dv	⊢ ( 𝑥 = 𝑋 → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) )
10	9	eqeq2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ↔ ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ) )
11		fveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐻 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑋 ) )
12	11	eqeq2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ↔ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) )
13	10 12	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ↔ ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) )
14	13	riotabidv	⊢ ( 𝑥 = 𝑋 → ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ) = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) )
15	14	fveq1d	⊢ ( 𝑥 = 𝑋 → ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑥 ) ) ) ‘ 𝑦 ) = ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑦 ) )
16		fveq2	⊢ ( 𝑦 = 𝑌 → ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑦 ) = ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑌 ) )
17		fvex	⊢ ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑌 ) ∈ V
18	15 16 7 17	ovmpo	⊢ ( ( 𝑋 ∈ ( 0 [,] 1 ) ∧ 𝑌 ∈ ( 0 [,] 1 ) ) → ( 𝑋 𝐾 𝑌 ) = ( ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑋 𝐺 𝑧 ) ) ∧ ( 𝑓 ‘ 0 ) = ( 𝐻 ‘ 𝑋 ) ) ) ‘ 𝑌 ) )