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		isphtpc	⊢ ( 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ↔ ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
10	9	bilani	⊢ ( ( 𝜑 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) → ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
11	10	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ( PHtpy ‘ 𝐽 ) 𝑥 ) ≠ ∅ ) )
12	11	simp2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → 𝑥 ∈ ( II Cn 𝐽 ) )
13		phtpc01	⊢ ( 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 → ( ( 𝑦 ‘ 0 ) = ( 𝑥 ‘ 0 ) ∧ ( 𝑦 ‘ 1 ) = ( 𝑥 ‘ 1 ) ) )
14	13	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( ( 𝑦 ‘ 0 ) = ( 𝑥 ‘ 0 ) ∧ ( 𝑦 ‘ 1 ) = ( 𝑥 ‘ 1 ) ) )
15	14	simpld	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ‘ 0 ) = ( 𝑥 ‘ 0 ) )
16	4 2 3 6	om1elbas	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐾 ↔ ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ‘ 0 ) = 𝑌 ∧ ( 𝑦 ‘ 1 ) = 𝑌 ) ) )
17	16	biimpa	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ‘ 0 ) = 𝑌 ∧ ( 𝑦 ‘ 1 ) = 𝑌 ) )
18	17	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ∈ ( II Cn 𝐽 ) ∧ ( 𝑦 ‘ 0 ) = 𝑌 ∧ ( 𝑦 ‘ 1 ) = 𝑌 ) )
19	18	simp2d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ‘ 0 ) = 𝑌 )
20	15 19	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑥 ‘ 0 ) = 𝑌 )
21	14	simprd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ‘ 1 ) = ( 𝑥 ‘ 1 ) )
22	18	simp3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑦 ‘ 1 ) = 𝑌 )
23	21 22	eqtr3d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑥 ‘ 1 ) = 𝑌 )
24	4 2 3 6	om1elbas	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 ↔ ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ‘ 0 ) = 𝑌 ∧ ( 𝑥 ‘ 1 ) = 𝑌 ) ) )
25	24	adantr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → ( 𝑥 ∈ 𝐾 ↔ ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ‘ 0 ) = 𝑌 ∧ ( 𝑥 ‘ 1 ) = 𝑌 ) ) )
26	12 20 23 25	mpbir3and	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐾 ∧ 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 ) ) → 𝑥 ∈ 𝐾 )
27	26	rexlimdvaa	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐾 𝑦 ( ≃ph ‘ 𝐽 ) 𝑥 → 𝑥 ∈ 𝐾 ) )
28	8 27	biimtrid	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) → 𝑥 ∈ 𝐾 ) )
29	28	ssrdv	⊢ ( 𝜑 → ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) ⊆ 𝐾 )
30		simp1	⊢ ( ( 𝑥 ∈ ( II Cn 𝐽 ) ∧ ( 𝑥 ‘ 0 ) = 𝑌 ∧ ( 𝑥 ‘ 1 ) = 𝑌 ) → 𝑥 ∈ ( II Cn 𝐽 ) )
31	24 30	biimtrdi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 → 𝑥 ∈ ( II Cn 𝐽 ) ) )
32	31	ssrdv	⊢ ( 𝜑 → 𝐾 ⊆ ( II Cn 𝐽 ) )
33	29 32	jca	⊢ ( 𝜑 → ( ( ( ≃ph ‘ 𝐽 ) “ 𝐾 ) ⊆ 𝐾 ∧ 𝐾 ⊆ ( II Cn 𝐽 ) ) )