Metamath Proof Explorer

Theorem om1val

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

Ref Expression
Hypotheses om1val.o 
|- O = ( J Om1 Y )
om1val.b 
|- ( ph -> B = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )
om1val.p 
|- ( ph -> .+ = ( *p ` J ) )
om1val.k 
|- ( ph -> K = ( J ^ko II ) )
om1val.j 
|- ( ph -> J e. ( TopOn ` X ) )
om1val.y 
|- ( ph -> Y e. X )
Assertion om1val 
|- ( ph -> O = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , K >. } )

Proof

Step Hyp Ref Expression
1 om1val.o 
 |-  O = ( J Om1 Y )
2 om1val.b 
 |-  ( ph -> B = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )
3 om1val.p 
 |-  ( ph -> .+ = ( *p ` J ) )
4 om1val.k 
 |-  ( ph -> K = ( J ^ko II ) )
5 om1val.j 
 |-  ( ph -> J e. ( TopOn ` X ) )
6 om1val.y 
 |-  ( ph -> Y e. X )
7 df-om1 
 |-  Om1 = ( j e. Top , y e. U. j |-> { <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >. , <. ( +g ` ndx ) , ( *p ` j ) >. , <. ( TopSet ` ndx ) , ( j ^ko II ) >. } )
8 7 a1i 
 |-  ( ph -> Om1 = ( j e. Top , y e. U. j |-> { <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >. , <. ( +g ` ndx ) , ( *p ` j ) >. , <. ( TopSet ` ndx ) , ( j ^ko II ) >. } ) )
9 simprl 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> j = J )
10 9 oveq2d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> ( II Cn j ) = ( II Cn J ) )
11 simprr 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> y = Y )
12 11 eqeq2d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> ( ( f ` 0 ) = y <-> ( f ` 0 ) = Y ) )
13 11 eqeq2d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> ( ( f ` 1 ) = y <-> ( f ` 1 ) = Y ) )
14 12 13 anbi12d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> ( ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) <-> ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) ) )
15 10 14 rabeqbidv 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )
16 2 adantr 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> B = { f e. ( II Cn J ) | ( ( f ` 0 ) = Y /\ ( f ` 1 ) = Y ) } )
17 15 16 eqtr4d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } = B )
18 17 opeq2d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >. = <. ( Base ` ndx ) , B >. )
19 9 fveq2d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> ( *p ` j ) = ( *p ` J ) )
20 3 adantr 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> .+ = ( *p ` J ) )
21 19 20 eqtr4d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> ( *p ` j ) = .+ )
22 21 opeq2d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> <. ( +g ` ndx ) , ( *p ` j ) >. = <. ( +g ` ndx ) , .+ >. )
23 9 oveq1d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> ( j ^ko II ) = ( J ^ko II ) )
24 4 adantr 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> K = ( J ^ko II ) )
25 23 24 eqtr4d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> ( j ^ko II ) = K )
26 25 opeq2d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> <. ( TopSet ` ndx ) , ( j ^ko II ) >. = <. ( TopSet ` ndx ) , K >. )
27 18 22 26 tpeq123d 
 |-  ( ( ph /\ ( j = J /\ y = Y ) ) -> { <. ( Base ` ndx ) , { f e. ( II Cn j ) | ( ( f ` 0 ) = y /\ ( f ` 1 ) = y ) } >. , <. ( +g ` ndx ) , ( *p ` j ) >. , <. ( TopSet ` ndx ) , ( j ^ko II ) >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , K >. } )
28 unieq 
 |-  ( j = J -> U. j = U. J )
29 28 adantl 
 |-  ( ( ph /\ j = J ) -> U. j = U. J )
30 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
31 5 30 syl 
 |-  ( ph -> X = U. J )
32 31 adantr 
 |-  ( ( ph /\ j = J ) -> X = U. J )
33 29 32 eqtr4d 
 |-  ( ( ph /\ j = J ) -> U. j = X )
34 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
35 5 34 syl 
 |-  ( ph -> J e. Top )
36 tpex 
 |-  { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , K >. } e. _V
37 36 a1i 
 |-  ( ph -> { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , K >. } e. _V )
38 8 27 33 35 6 37 ovmpodx 
 |-  ( ph -> ( J Om1 Y ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , K >. } )
39 1 38 syl5eq 
 |-  ( ph -> O = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , K >. } )