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		isphtpc	$⊢ y ≃_{ph} (J) x \leftrightarrow (y \in (II Cn J) \land x \in (II Cn J) \land y PHtpy (J) x \neq \emptyset)$
10	9	bilani	$⊢ (φ \land y ≃_{ph} (J) x) \to (y \in (II Cn J) \land x \in (II Cn J) \land y PHtpy (J) x \neq \emptyset)$
11	10	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)$
12	11	simp2d	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to x \in (II Cn J)$
13		phtpc01	$⊢ y ≃_{ph} (J) x \to (y (0) = x (0) \land y (1) = x (1))$
14	13	ad2antll	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to (y (0) = x (0) \land y (1) = x (1))$
15	14	simpld	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to y (0) = x (0)$
16	4 2 3 6	om1elbas	$⊢ φ \to (y \in K \leftrightarrow (y \in (II Cn J) \land y (0) = Y \land y (1) = Y))$
17	16	biimpa	$⊢ (φ \land y \in K) \to (y \in (II Cn J) \land y (0) = Y \land y (1) = Y)$
18	17	adantrr	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to (y \in (II Cn J) \land y (0) = Y \land y (1) = Y)$
19	18	simp2d	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to y (0) = Y$
20	15 19	eqtr3d	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to x (0) = Y$
21	14	simprd	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to y (1) = x (1)$
22	18	simp3d	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to y (1) = Y$
23	21 22	eqtr3d	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to x (1) = Y$
24	4 2 3 6	om1elbas	$⊢ φ \to (x \in K \leftrightarrow (x \in (II Cn J) \land x (0) = Y \land x (1) = Y))$
25	24	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))$
26	12 20 23 25	mpbir3and	$⊢ (φ \land (y \in K \land y ≃_{ph} (J) x)) \to x \in K$
27	26	rexlimdvaa	$⊢ φ \to (\exists y \in K y ≃_{ph} (J) x \to x \in K)$
28	8 27	biimtrid	$⊢ φ \to (x \in ≃_{ph} (J) [K] \to x \in K)$
29	28	ssrdv	$⊢ φ \to ≃_{ph} (J) [K] \subseteq K$
30		simp1	$⊢ (x \in (II Cn J) \land x (0) = Y \land x (1) = Y) \to x \in (II Cn J)$
31	24 30	biimtrdi	$⊢ φ \to (x \in K \to x \in (II Cn J))$
32	31	ssrdv	$⊢ φ \to K \subseteq II Cn J$
33	29 32	jca	$⊢ φ \to (≃_{ph} (J) [K] \subseteq K \land K \subseteq II Cn J)$

Metamath Proof Explorer

Theorem pi1blem

Proof