Theorem cvmlift3lem1

Description: Lemma for cvmlift3 . (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	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
	cvmlift3lem1.1	⊢ ( 𝜑 → 𝑀 ∈ ( II Cn 𝐾 ) )
	cvmlift3lem1.2	⊢ ( 𝜑 → ( 𝑀 ‘ 0 ) = 𝑂 )
	cvmlift3lem1.3	⊢ ( 𝜑 → 𝑁 ∈ ( II Cn 𝐾 ) )
	cvmlift3lem1.4	⊢ ( 𝜑 → ( 𝑁 ‘ 0 ) = 𝑂 )
	cvmlift3lem1.5	⊢ ( 𝜑 → ( 𝑀 ‘ 1 ) = ( 𝑁 ‘ 1 ) )
Assertion	cvmlift3lem1	⊢ ( 𝜑 → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑀 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) )

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		cvmlift3lem1.1	⊢ ( 𝜑 → 𝑀 ∈ ( II Cn 𝐾 ) )
11		cvmlift3lem1.2	⊢ ( 𝜑 → ( 𝑀 ‘ 0 ) = 𝑂 )
12		cvmlift3lem1.3	⊢ ( 𝜑 → 𝑁 ∈ ( II Cn 𝐾 ) )
13		cvmlift3lem1.4	⊢ ( 𝜑 → ( 𝑁 ‘ 0 ) = 𝑂 )
14		cvmlift3lem1.5	⊢ ( 𝜑 → ( 𝑀 ‘ 1 ) = ( 𝑁 ‘ 1 ) )
15		eqid	⊢ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑀 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑀 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
16		eqid	⊢ ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
17	11	fveq2d	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑀 ‘ 0 ) ) = ( 𝐺 ‘ 𝑂 ) )
18	9 17	eqtr4d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ ( 𝑀 ‘ 0 ) ) )
19		iiuni	⊢ ( 0 [,] 1 ) = ∪ II
20	19 2	cnf	⊢ ( 𝑀 ∈ ( II Cn 𝐾 ) → 𝑀 : ( 0 [,] 1 ) ⟶ 𝑌 )
21	10 20	syl	⊢ ( 𝜑 → 𝑀 : ( 0 [,] 1 ) ⟶ 𝑌 )
22		0elunit	⊢ 0 ∈ ( 0 [,] 1 )
23		fvco3	⊢ ( ( 𝑀 : ( 0 [,] 1 ) ⟶ 𝑌 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 𝐺 ∘ 𝑀 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑀 ‘ 0 ) ) )
24	21 22 23	sylancl	⊢ ( 𝜑 → ( ( 𝐺 ∘ 𝑀 ) ‘ 0 ) = ( 𝐺 ‘ ( 𝑀 ‘ 0 ) ) )
25	18 24	eqtr4d	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( ( 𝐺 ∘ 𝑀 ) ‘ 0 ) )
26	11 13	eqtr4d	⊢ ( 𝜑 → ( 𝑀 ‘ 0 ) = ( 𝑁 ‘ 0 ) )
27	4 10 12 26 14	sconnpht2	⊢ ( 𝜑 → 𝑀 ( ≃ph ‘ 𝐾 ) 𝑁 )
28	27 7	phtpcco2	⊢ ( 𝜑 → ( 𝐺 ∘ 𝑀 ) ( ≃ph ‘ 𝐽 ) ( 𝐺 ∘ 𝑁 ) )
29	1 15 16 3 8 25 28	cvmliftpht	⊢ ( 𝜑 → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑀 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ( ≃ph ‘ 𝐶 ) ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
30		phtpc01	⊢ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑀 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ( ≃ph ‘ 𝐶 ) ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑀 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 0 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 0 ) ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑀 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) )
31	29 30	syl	⊢ ( 𝜑 → ( ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑀 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 0 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 0 ) ∧ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑀 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) ) )
32	31	simprd	⊢ ( 𝜑 → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑀 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝐺 ∘ 𝑁 ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) ‘ 1 ) )