pi1blem

	Ref	Expression
Hypotheses	pi1val.g	$⊢ G = J π_{1} Y$
	pi1val.1	$⊢ φ \to J \in TopOn (X)$
	pi1val.2	$⊢ φ \to Y \in X$
	pi1val.o	$⊢ O = J Ω_{1} Y$
	pi1bas.b	$⊢ φ \to B = {Base}_{G}$
	pi1bas.k	$⊢ φ \to K = {Base}_{O}$
Assertion	pi1blem	$⊢ φ \to (≃_{ph} (J) [K] \subseteq K \land K \subseteq II Cn J)$

Proof

Step	Hyp	Ref	Expression
1		pi1val.g	$⊢ G = J π_{1} Y$
2		pi1val.1	$⊢ φ \to J \in TopOn (X)$
3		pi1val.2	$⊢ φ \to Y \in X$
4		pi1val.o	$⊢ O = J Ω_{1} Y$
5		pi1bas.b	$⊢ φ \to B = {Base}_{G}$
6		pi1bas.k	$⊢ φ \to K = {Base}_{O}$
7		vex	$⊢ x \in V$
8	7	elima	$⊢ x \in ≃_{ph} (J) [K] \leftrightarrow \exists y \in K y ≃_{ph} (J) x$
9		simpr	$⊢ (φ \land y ≃_{ph} (J) x) \to y ≃_{ph} (J) x$
10		isphtpc	$⊢ y ≃_{ph} (J) x \leftrightarrow (y \in (II Cn J) \land x \in (II Cn J) \land y PHtpy (J) x \neq \emptyset)$
11	9 10	sylib	$⊢ (φ \land y ≃_{ph} (J) x) \to (y \in (II Cn J) \land x \in (II Cn J) \land y PHtpy (J) x \neq \emptyset)$
12	11	adantrl	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to (y \in (II Cn J) \land x \in (II Cn J) \land y PHtpy (J) x \neq \emptyset)$
13	12	simp2d	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to x \in (II Cn J)$
14		phtpc01	$⊢ y ≃_{ph} (J) x \to (y (0) = x (0) \land y (1) = x (1))$
15	14	ad2antll	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to (y (0) = x (0) \land y (1) = x (1))$
16	15	simpld	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to y (0) = x (0)$
17	4 2 3 6	om1elbas	$⊢ φ \to (y \in K \leftrightarrow (y \in (II Cn J) \land y (0) = Y \land y (1) = Y))$
18	17	biimpa	$⊢ (φ \land y \in K) \to (y \in (II Cn J) \land y (0) = Y \land y (1) = Y)$
19	18	adantrr	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to (y \in (II Cn J) \land y (0) = Y \land y (1) = Y)$
20	19	simp2d	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to y (0) = Y$
21	16 20	eqtr3d	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to x (0) = Y$
22	15	simprd	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to y (1) = x (1)$
23	19	simp3d	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to y (1) = Y$
24	22 23	eqtr3d	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to x (1) = Y$
25	4 2 3 6	om1elbas	$⊢ φ \to (x \in K \leftrightarrow (x \in (II Cn J) \land x (0) = Y \land x (1) = Y))$
26	25	adantr	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to (x \in K \leftrightarrow (x \in (II Cn J) \land x (0) = Y \land x (1) = Y))$
27	13 21 24 26	mpbir3and	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to x \in K$
28	27	rexlimdvaa	$⊢ φ \to (\exists y \in K y ≃_{ph} (J) x \to x \in K)$
29	8 28	syl5bi	$⊢ φ \to (x \in ≃_{ph} (J) [K] \to x \in K)$
30	29	ssrdv	$⊢ φ \to ≃_{ph} (J) [K] \subseteq K$
31		simp1	$⊢ (x \in (II Cn J) \land x (0) = Y \land x (1) = Y) \to x \in (II Cn J)$
32	25 31	syl6bi	$⊢ φ \to (x \in K \to x \in (II Cn J))$
33	32	ssrdv	$⊢ φ \to K \subseteq II Cn J$
34	30 33	jca	$⊢ φ \to (≃_{ph} (J) [K] \subseteq K \land K \subseteq II Cn J)$

Metamath Proof Explorer

Theorem pi1blem

Proof