Theorem cvmlift3lem3

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 6-Jul-2015)

	Ref	Expression
Hypotheses	cvmlift3.b	⊢ 𝐵 = ∪ 𝐶
	cvmlift3.y	⊢ 𝑌 = ∪ 𝐾
	cvmlift3.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
	cvmlift3.k	⊢ ( 𝜑 → 𝐾 ∈ SConn )
	cvmlift3.l	⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally PConn )
	cvmlift3.o	⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
	cvmlift3.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
	cvmlift3.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
	cvmlift3.e	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
	cvmlift3.h	⊢ 𝐻 = ( 𝑥 ∈ 𝑌 ↦ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
Assertion	cvmlift3lem3	⊢ ( 𝜑 → 𝐻 : 𝑌 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cvmlift3.b	⊢ 𝐵 = ∪ 𝐶
2		cvmlift3.y	⊢ 𝑌 = ∪ 𝐾
3		cvmlift3.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
4		cvmlift3.k	⊢ ( 𝜑 → 𝐾 ∈ SConn )
5		cvmlift3.l	⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally PConn )
6		cvmlift3.o	⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
7		cvmlift3.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
8		cvmlift3.p	⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
9		cvmlift3.e	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
10		cvmlift3.h	⊢ 𝐻 = ( 𝑥 ∈ 𝑌 ↦ ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) )
11	1 2 3 4 5 6 7 8 9	cvmlift3lem2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ∃! 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) )
12		riotacl	⊢ ( ∃! 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) → ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) ∈ 𝐵 )
13	11 12	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑌 ) → ( ℩ 𝑧 ∈ 𝐵 ∃ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = 𝑂 ∧ ( 𝑓 ‘ 1 ) = 𝑥 ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑓 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = 𝑧 ) ) ∈ 𝐵 )
14	13 10	fmptd	⊢ ( 𝜑 → 𝐻 : 𝑌 ⟶ 𝐵 )