Metamath Proof Explorer

Theorem odfvalALT

Description: Shorter proof of odfval using ax-rep . (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by AV, 5-Oct-2020) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses odval.1 
|- X = ( Base ` G )
odval.2 
|- .x. = ( .g ` G )
odval.3 
|- .0. = ( 0g ` G )
odval.4 
|- O = ( od ` G )
Assertion odfvalALT 
|- 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 15 16 1 mptfvmpt 
 |-  ( G e. _V -> ( od ` G ) = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )
18 fvprc 
 |-  ( -. G e. _V -> ( od ` G ) = (/) )
19 fvprc 
 |-  ( -. G e. _V -> ( Base ` G ) = (/) )
20 1 19 eqtrid 
 |-  ( -. G e. _V -> X = (/) )
21 20 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 , < ) ) ) )
22 mpt0 
 |-  ( x e. (/) |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) = (/)
23 21 22 eqtrdi 
 |-  ( -. G e. _V -> ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) = (/) )
24 18 23 eqtr4d 
 |-  ( -. G e. _V -> ( od ` G ) = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) ) )
25 17 24 pm2.61i 
 |-  ( od ` G ) = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )
26 4 25 eqtri 
 |-  O = ( x e. X |-> [_ { y e. NN | ( y .x. x ) = .0. } / i ]_ if ( i = (/) , 0 , inf ( i , RR , < ) ) )