Metamath Proof Explorer

Theorem inftmrel

Description: The infinitesimal relation for a structure W . (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypothesis inftm.b 
|- B = ( Base ` W )
Assertion inftmrel 
|- ( W e. V -> ( <<< ` W ) C_ ( B X. B ) )

Proof

Step Hyp Ref Expression
1 inftm.b 
 |-  B = ( Base ` W )
2 elex 
 |-  ( W e. V -> W e. _V )
3 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
4 3 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = B )
5 4 eleq2d 
 |-  ( w = W -> ( x e. ( Base ` w ) <-> x e. B ) )
6 4 eleq2d 
 |-  ( w = W -> ( y e. ( Base ` w ) <-> y e. B ) )
7 5 6 anbi12d 
 |-  ( w = W -> ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) <-> ( x e. B /\ y e. B ) ) )
8 fveq2 
 |-  ( w = W -> ( 0g ` w ) = ( 0g ` W ) )
9 fveq2 
 |-  ( w = W -> ( lt ` w ) = ( lt ` W ) )
10 eqidd 
 |-  ( w = W -> x = x )
11 8 9 10 breq123d 
 |-  ( w = W -> ( ( 0g ` w ) ( lt ` w ) x <-> ( 0g ` W ) ( lt ` W ) x ) )
12 fveq2 
 |-  ( w = W -> ( .g ` w ) = ( .g ` W ) )
13 12 oveqd 
 |-  ( w = W -> ( n ( .g ` w ) x ) = ( n ( .g ` W ) x ) )
14 eqidd 
 |-  ( w = W -> y = y )
15 13 9 14 breq123d 
 |-  ( w = W -> ( ( n ( .g ` w ) x ) ( lt ` w ) y <-> ( n ( .g ` W ) x ) ( lt ` W ) y ) )
16 15 ralbidv 
 |-  ( w = W -> ( A. n e. NN ( n ( .g ` w ) x ) ( lt ` w ) y <-> A. n e. NN ( n ( .g ` W ) x ) ( lt ` W ) y ) )
17 11 16 anbi12d 
 |-  ( w = W -> ( ( ( 0g ` w ) ( lt ` w ) x /\ A. n e. NN ( n ( .g ` w ) x ) ( lt ` w ) y ) <-> ( ( 0g ` W ) ( lt ` W ) x /\ A. n e. NN ( n ( .g ` W ) x ) ( lt ` W ) y ) ) )
18 7 17 anbi12d 
 |-  ( w = W -> ( ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( ( 0g ` w ) ( lt ` w ) x /\ A. n e. NN ( n ( .g ` w ) x ) ( lt ` w ) y ) ) <-> ( ( x e. B /\ y e. B ) /\ ( ( 0g ` W ) ( lt ` W ) x /\ A. n e. NN ( n ( .g ` W ) x ) ( lt ` W ) y ) ) ) )
19 18 opabbidv 
 |-  ( w = W -> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( ( 0g ` w ) ( lt ` w ) x /\ A. n e. NN ( n ( .g ` w ) x ) ( lt ` w ) y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( ( 0g ` W ) ( lt ` W ) x /\ A. n e. NN ( n ( .g ` W ) x ) ( lt ` W ) y ) ) } )
20 df-inftm 
 |-  <<< = ( w e. _V |-> { <. x , y >. | ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( ( 0g ` w ) ( lt ` w ) x /\ A. n e. NN ( n ( .g ` w ) x ) ( lt ` w ) y ) ) } )
21 1 fvexi 
 |-  B e. _V
22 21 21 xpex 
 |-  ( B X. B ) e. _V
23 opabssxp 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( ( 0g ` W ) ( lt ` W ) x /\ A. n e. NN ( n ( .g ` W ) x ) ( lt ` W ) y ) ) } C_ ( B X. B )
24 22 23 ssexi 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( ( 0g ` W ) ( lt ` W ) x /\ A. n e. NN ( n ( .g ` W ) x ) ( lt ` W ) y ) ) } e. _V
25 19 20 24 fvmpt 
 |-  ( W e. _V -> ( <<< ` W ) = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( ( 0g ` W ) ( lt ` W ) x /\ A. n e. NN ( n ( .g ` W ) x ) ( lt ` W ) y ) ) } )
26 2 25 syl 
 |-  ( W e. V -> ( <<< ` W ) = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( ( 0g ` W ) ( lt ` W ) x /\ A. n e. NN ( n ( .g ` W ) x ) ( lt ` W ) y ) ) } )
27 26 23 eqsstrdi 
 |-  ( W e. V -> ( <<< ` W ) C_ ( B X. B ) )