Theorem pi1blem

Description: Lemma for pi1buni . (Contributed by Mario Carneiro, 10-Jul-2015)

	Ref	Expression
Hypotheses	pi1val.g	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
	pi1val.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	pi1val.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
	pi1val.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
	pi1bas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
	pi1bas.k	⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝑂 ) )
Assertion	pi1blem	⊢ ( 𝜑 → ( ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ( II Cn 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pi1val.g	⊢ 𝐺 = ( 𝐽 π1 𝑌 )
2		pi1val.1	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3		pi1val.2	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
4		pi1val.o	⊢ 𝑂 = ( 𝐽 Ω1 𝑌 )
5		pi1bas.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
6		pi1bas.k	⊢ ( 𝜑 → 𝐾 = ( Base ‘ 𝑂 ) )
7		vex	⊢ 𝑥 ∈ V
8	7	elima	⊢ ( 𝑥 ∈ ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) ↔ ∃ 𝑦 ∈ 𝐾 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 )
9		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) → 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 )
10		isphtpc	⊢ ( 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ↔ ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
11	9 10	sylib	⊢ ( ( 𝜑 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) → ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
12	11	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
13	12	simp2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → 𝑥 ∈ ( II Cn 𝐽 ) )
14		phtpc01	⊢ ( 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 → ( ( 𝑦 ‘ 0 ) = ( 𝑥 ‘ 0 ) ∧ ( 𝑦 ‘ 1 ) = ( 𝑥 ‘ 1 ) ) )
15	14	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( ( 𝑦 ‘ 0 ) = ( 𝑥 ‘ 0 ) ∧ ( 𝑦 ‘ 1 ) = ( 𝑥 ‘ 1 ) ) )
16	15	simpld	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ‘ 0 ) = ( 𝑥 ‘ 0 ) )
17	4 2 3 6	om1elbas	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 ↔ ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ‘ 0 ) = 𝑌 ∧ ( 𝑦 ‘ 1 ) = 𝑌 ) ) )
18	17	biimpa	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ‘ 0 ) = 𝑌 ∧ ( 𝑦 ‘ 1 ) = 𝑌 ) )
19	18	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ‘ 0 ) = 𝑌 ∧ ( 𝑦 ‘ 1 ) = 𝑌 ) )
20	19	simp2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ‘ 0 ) = 𝑌 )
21	16 20	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑥 ‘ 0 ) = 𝑌 )
22	15	simprd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ‘ 1 ) = ( 𝑥 ‘ 1 ) )
23	19	simp3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ‘ 1 ) = 𝑌 )
24	22 23	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑥 ‘ 1 ) = 𝑌 )
25	4 2 3 6	om1elbas	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 ↔ ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ‘ 0 ) = 𝑌 ∧ ( 𝑥 ‘ 1 ) = 𝑌 ) ) )
26	25	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑥 ∈ 𝐾 ↔ ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ‘ 0 ) = 𝑌 ∧ ( 𝑥 ‘ 1 ) = 𝑌 ) ) )
27	13 21 24 26	mpbir3and	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → 𝑥 ∈ 𝐾 )
28	27	rexlimdvaa	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐾 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 → 𝑥 ∈ 𝐾 ) )
29	8 28	syl5bi	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) → 𝑥 ∈ 𝐾 ) )
30	29	ssrdv	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) ⊆ 𝐾 )
31		simp1	⊢ ( ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ‘ 0 ) = 𝑌 ∧ ( 𝑥 ‘ 1 ) = 𝑌 ) → 𝑥 ∈ ( II Cn 𝐽 ) )
32	25 31	syl6bi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 → 𝑥 ∈ ( II Cn 𝐽 ) ) )
33	32	ssrdv	⊢ ( 𝜑 → 𝐾 ⊆ ( II Cn 𝐽 ) )
34	30 33	jca	⊢ ( 𝜑 → ( ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ( II Cn 𝐽 ) ) )