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 Om1 Y )
om1bas.j 
|- ( ph -> J e. ( TopOn ` X ) )
om1bas.y 
|- ( ph -> Y e. X )
om1bas.b 
|- ( ph -> B = ( Base ` O ) )
Assertion om1bas 
|- ( ph -> B = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )

Proof

Step Hyp Ref Expression
1 om1bas.o 
 |-  O = ( J Om1 Y )
2 om1bas.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 om1bas.y 
 |-  ( ph -> Y e. X )
4 om1bas.b 
 |-  ( ph -> B = ( Base ` O ) )
5 eqidd 
 |-  ( ph -> { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )
6 eqidd 
 |-  ( ph -> ( *p ` J ) = ( *p ` J ) )
7 eqidd 
 |-  ( ph -> ( J ^ko II ) = ( J ^ko II ) )
8 1 5 6 7 2 3 om1val 
 |-  ( ph -> O = { <. ( Base ` ndx ) , { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } )
9 8 fveq2d 
 |-  ( ph -> ( Base ` O ) = ( Base ` { <. ( Base ` ndx ) , { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } ) )
10 4 9 eqtrd 
 |-  ( ph -> B = ( Base ` { <. ( Base ` ndx ) , { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } ) )
11 ovex 
 |-  ( II Cn J ) e. _V
12 11 rabex 
 |-  { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } e. _V
13 eqid 
 |-  { <. ( Base ` ndx ) , { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } = { <. ( Base ` ndx ) , { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. }
14 13 topgrpbas 
 |-  ( { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } e. _V -> { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } = ( Base ` { <. ( Base ` ndx ) , { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } ) )
15 12 14 ax-mp 
 |-  { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } = ( Base ` { <. ( Base ` ndx ) , { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } >. , <. ( +g ` ndx ) , ( *p ` J ) >. , <. ( TopSet ` ndx ) , ( J ^ko II ) >. } )
16 10 15 eqtr4di 
 |-  ( ph -> B = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )