om1addcl

Description: Closure of the group operation of the loop space. (Contributed by Jeff Madsen, 11-Jun-2010) (Revised by Mario Carneiro, 5-Sep-2015)

Step	Hyp	Ref	Expression
1		om1bas.o	$⊢ O = J Ω_{1} Y$
2		om1bas.j	$⊢ φ \to J \in TopOn (X)$
3		om1bas.y	$⊢ φ \to Y \in X$
4		om1bas.b	$⊢ φ \to B = {Base}_{O}$
5		om1addcl.h	$⊢ φ \to H \in B$
6		om1addcl.k	$⊢ φ \to K \in B$
7	1 2 3 4	om1elbas	$⊢ φ \to (H \in B \leftrightarrow (H \in (II Cn J) \land H (0) = Y \land H (1) = Y))$
8	5 7	mpbid	$⊢ φ \to (H \in (II Cn J) \land H (0) = Y \land H (1) = Y)$
9	8	simp1d	$⊢ φ \to H \in (II Cn J)$
10	1 2 3 4	om1elbas	$⊢ φ \to (K \in B \leftrightarrow (K \in (II Cn J) \land K (0) = Y \land K (1) = Y))$
11	6 10	mpbid	$⊢ φ \to (K \in (II Cn J) \land K (0) = Y \land K (1) = Y)$
12	11	simp1d	$⊢ φ \to K \in (II Cn J)$
13	8	simp3d	$⊢ φ \to H (1) = Y$
14	11	simp2d	$⊢ φ \to K (0) = Y$
15	13 14	eqtr4d	$⊢ φ \to H (1) = K (0)$
16	9 12 15	pcocn	$⊢ φ \to H *_{𝑝} (J) K \in (II Cn J)$
17	9 12	pco0	$⊢ φ \to (H *_{𝑝} (J) K) (0) = H (0)$
18	8	simp2d	$⊢ φ \to H (0) = Y$
19	17 18	eqtrd	$⊢ φ \to (H *_{𝑝} (J) K) (0) = Y$
20	9 12	pco1	$⊢ φ \to (H *_{𝑝} (J) K) (1) = K (1)$
21	11	simp3d	$⊢ φ \to K (1) = Y$
22	20 21	eqtrd	$⊢ φ \to (H *_{𝑝} (J) K) (1) = Y$
23	1 2 3 4	om1elbas	$⊢ φ \to (H _{𝑝} (J) K \in B \leftrightarrow (H _{𝑝} (J) K \in (II Cn J) \land (H _{𝑝} (J) K) (0) = Y \land (H _{𝑝} (J) K) (1) = Y))$
24	16 19 22 23	mpbir3and	$⊢ φ \to H *_{𝑝} (J) K \in B$

Metamath Proof Explorer