Metamath Proof Explorer

Theorem om1bas

Description: The base set of the loop space. (Contributed by Mario Carneiro, 10-Jul-2015)

Ref Expression
Hypotheses om1bas.o ⊢ O = J Ω 1 Y
om1bas.j ⊢ φ → J ∈ TopOn ⁡ X
om1bas.y ⊢ φ → Y ∈ X
om1bas.b ⊢ φ → B = Base O
Assertion om1bas ⊢ φ → B = f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y

Proof

Step Hyp Ref Expression
1 om1bas.o ⊢ O = J Ω 1 Y
2 om1bas.j ⊢ φ → J ∈ TopOn ⁡ X
3 om1bas.y ⊢ φ → Y ∈ X
4 om1bas.b ⊢ φ → B = Base O
5 eqidd ⊢ φ → f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y = f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y
6 eqidd ⊢ φ → * 𝑝 ⁡ J = * 𝑝 ⁡ J
7 eqidd ⊢ φ → J ^ ko II = J ^ ko II
8 1 5 6 7 2 3 om1val ⊢ φ → O = Base ndx f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y + ndx * 𝑝 ⁡ J TopSet ⁡ ndx J ^ ko II
9 8 fveq2d ⊢ φ → Base O = Base Base ndx f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y + ndx * 𝑝 ⁡ J TopSet ⁡ ndx J ^ ko II
10 4 9 eqtrd ⊢ φ → B = Base Base ndx f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y + ndx * 𝑝 ⁡ J TopSet ⁡ ndx J ^ ko II
11 ovex ⊢ II Cn J ∈ V
12 11 rabex ⊢ f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y ∈ V
13 eqid ⊢ Base ndx f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y + ndx * 𝑝 ⁡ J TopSet ⁡ ndx J ^ ko II = Base ndx f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y + ndx * 𝑝 ⁡ J TopSet ⁡ ndx J ^ ko II
14 13 topgrpbas ⊢ f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y ∈ V → f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y = Base Base ndx f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y + ndx * 𝑝 ⁡ J TopSet ⁡ ndx J ^ ko II
15 12 14 ax-mp ⊢ f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y = Base Base ndx f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y + ndx * 𝑝 ⁡ J TopSet ⁡ ndx J ^ ko II
16 10 15 eqtr4di ⊢ φ → B = f ∈ II Cn J | f ⁡ 0 = Y ∧ f ⁡ 1 = Y