Metamath Proof Explorer

Theorem odfval

Description: Value of the order function. For a shorter proof using ax-rep , see odfvalALT . (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by AV, 5-Oct-2020) Remove dependency on ax-rep . (Revised by Rohan Ridenour, 17-Aug-2023)

Ref Expression
Hypotheses odval.1 
|- X = ( Base ` G )
odval.2 
|- .x. = ( .g ` G )
odval.3 
|- .0. = ( 0g ` G )
odval.4 
|- O = ( od ` G )
Assertion odfval 
|- O = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )

Proof

Step Hyp Ref Expression
1 odval.1 
 |-  X = ( Base ` G )
2 odval.2 
 |-  .x. = ( .g ` G )
3 odval.3 
 |-  .0. = ( 0g ` G )
4 odval.4 
 |-  O = ( od ` G )
5 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
6 5 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = X )
7 fveq2 
 |-  ( g = G -> ( .g ` g ) = ( .g ` G ) )
8 7 2 eqtr4di 
 |-  ( g = G -> ( .g ` g ) = .x. )
9 8 oveqd 
 |-  ( g = G -> ( y ( .g ` g ) x ) = ( y .x. x ) )
10 fveq2 
 |-  ( g = G -> ( 0g ` g ) = ( 0g ` G ) )
11 10 3 eqtr4di 
 |-  ( g = G -> ( 0g ` g ) = .0. )
12 9 11 eqeq12d 
 |-  ( g = G -> ( ( y ( .g ` g ) x ) = ( 0g ` g ) <-> ( y .x. x ) = .0. ) )
13 12 rabbidv 
 |-  ( g = G -> { y e. NN | ( y ( .g ` g ) x ) = ( 0g ` g ) } = { y e. NN | ( y .x. x ) = .0. } )
14 13 csbeq1d 
 |-  ( g = G -> [_ { y e. NN | ( y ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) = [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )
15 6 14 mpteq12dv 
 |-  ( g = G -> ( x e. ( Base ` g ) |-> [_ { y e. NN | ( y ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )
16 df-od 
 |-  od = ( g e. _V |-> ( x e. ( Base ` g ) |-> [_ { y e. NN | ( y ( .g ` g ) x ) = ( 0g ` g ) } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )
17 1 fvexi 
 |-  X e. _V
18 nn0ex 
 |-  NN0 e. _V
19 nnex 
 |-  NN e. _V
20 19 rabex 
 |-  { y e. NN | ( y .x. x ) = .0. } e. _V
21 eqeq1 
 |-  ( i = { y e. NN | ( y .x. x ) = .0. } -> ( i = (/) <-> { y e. NN | ( y .x. x ) = .0. } = (/) ) )
22 infeq1 
 |-  ( i = { y e. NN | ( y .x. x ) = .0. } -> inf ( i , RR , < ) = inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) )
23 21 22 ifbieq2d 
 |-  ( i = { y e. NN | ( y .x. x ) = .0. } -> if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( { y e. NN | ( y .x. x ) = .0. } = (/) , 0 , inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) ) )
24 20 23 csbie 
 |-  [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) = if ( { y e. NN | ( y .x. x ) = .0. } = (/) , 0 , inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) )
25 0nn0 
 |-  0 e. NN0
26 25 a1i 
 |-  ( ( T. /\ { y e. NN | ( y .x. x ) = .0. } = (/) ) -> 0 e. NN0 )
27 df-ne 
 |-  ( { y e. NN | ( y .x. x ) = .0. } =/= (/) <-> -. { y e. NN | ( y .x. x ) = .0. } = (/) )
28 ssrab2 
 |-  { y e. NN | ( y .x. x ) = .0. } C_ NN
29 nnuz 
 |-  NN = ( ZZ>= ` 1 )
30 28 29 sseqtri 
 |-  { y e. NN | ( y .x. x ) = .0. } C_ ( ZZ>= ` 1 )
31 infssuzcl 
 |-  ( ( { y e. NN | ( y .x. x ) = .0. } C_ ( ZZ>= ` 1 ) /\ { y e. NN | ( y .x. x ) = .0. } =/= (/) ) -> inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) e. { y e. NN | ( y .x. x ) = .0. } )
32 30 31 mpan 
 |-  ( { y e. NN | ( y .x. x ) = .0. } =/= (/) -> inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) e. { y e. NN | ( y .x. x ) = .0. } )
33 28 32 sselid 
 |-  ( { y e. NN | ( y .x. x ) = .0. } =/= (/) -> inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) e. NN )
34 27 33 sylbir 
 |-  ( -. { y e. NN | ( y .x. x ) = .0. } = (/) -> inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) e. NN )
35 34 nnnn0d 
 |-  ( -. { y e. NN | ( y .x. x ) = .0. } = (/) -> inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) e. NN0 )
36 35 adantl 
 |-  ( ( T. /\ -. { y e. NN | ( y .x. x ) = .0. } = (/) ) -> inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) e. NN0 )
37 26 36 ifclda 
 |-  ( T. -> if ( { y e. NN | ( y .x. x ) = .0. } = (/) , 0 , inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) ) e. NN0 )
38 37 mptru 
 |-  if ( { y e. NN | ( y .x. x ) = .0. } = (/) , 0 , inf ( { y e. NN | ( y .x. x ) = .0. } , RR , < ) ) e. NN0
39 24 38 eqeltri 
 |-  [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) e. NN0
40 39 rgenw 
 |-  A. x e. X [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) e. NN0
41 17 18 40 mptexw 
 |-  ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) e. _V
42 15 16 41 fvmpt 
 |-  ( G e. _V -> ( od ` G ) = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )
43 fvprc 
 |-  ( -. G e. _V -> ( od ` G ) = (/) )
44 fvprc 
 |-  ( -. G e. _V -> ( Base ` G ) = (/) )
45 1 44 eqtrid 
 |-  ( -. G e. _V -> X = (/) )
46 45 mpteq1d 
 |-  ( -. G e. _V -> ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) = ( x e. (/) |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )
47 mpt0 
 |-  ( x e. (/) |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) = (/)
48 46 47 eqtrdi 
 |-  ( -. G e. _V -> ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) = (/) )
49 43 48 eqtr4d 
 |-  ( -. G e. _V -> ( od ` G ) = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )
50 42 49 pm2.61i 
 |-  ( od ` G ) = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )
51 4 50 eqtri 
 |-  O = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )