Metamath Proof Explorer

Theorem isinftm

Description: Express x is infinitesimal with respect to y for a structure W . (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses inftm.b 
|- B = ( Base ` W )
inftm.0 
|- .0. = ( 0g ` W )
inftm.x 
|- .x. = ( .g ` W )
inftm.l 
|- .< = ( lt ` W )
Assertion isinftm 
|- ( ( W e. V /\ X e. B /\ Y e. B ) -> ( X ( <<< ` W ) Y <-> ( .0. .< X /\ A. n e. NN ( n .x. X ) .< Y ) ) )

Proof

Step Hyp Ref Expression
1 inftm.b 
 |-  B = ( Base ` W )
2 inftm.0 
 |-  .0. = ( 0g ` W )
3 inftm.x 
 |-  .x. = ( .g ` W )
4 inftm.l 
 |-  .< = ( lt ` W )
5 eleq1 
 |-  ( x = X -> ( x e. B <-> X e. B ) )
6 eleq1 
 |-  ( y = Y -> ( y e. B <-> Y e. B ) )
7 5 6 bi2anan9 
 |-  ( ( x = X /\ y = Y ) -> ( ( x e. B /\ y e. B ) <-> ( X e. B /\ Y e. B ) ) )
8 simpl 
 |-  ( ( x = X /\ y = Y ) -> x = X )
9 8 breq2d 
 |-  ( ( x = X /\ y = Y ) -> ( .0. .< x <-> .0. .< X ) )
10 8 oveq2d 
 |-  ( ( x = X /\ y = Y ) -> ( n .x. x ) = ( n .x. X ) )
11 simpr 
 |-  ( ( x = X /\ y = Y ) -> y = Y )
12 10 11 breq12d 
 |-  ( ( x = X /\ y = Y ) -> ( ( n .x. x ) .< y <-> ( n .x. X ) .< Y ) )
13 12 ralbidv 
 |-  ( ( x = X /\ y = Y ) -> ( A. n e. NN ( n .x. x ) .< y <-> A. n e. NN ( n .x. X ) .< Y ) )
14 9 13 anbi12d 
 |-  ( ( x = X /\ y = Y ) -> ( ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) <-> ( .0. .< X /\ A. n e. NN ( n .x. X ) .< Y ) ) )
15 7 14 anbi12d 
 |-  ( ( x = X /\ y = Y ) -> ( ( ( x e. B /\ y e. B ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) <-> ( ( X e. B /\ Y e. B ) /\ ( .0. .< X /\ A. n e. NN ( n .x. X ) .< Y ) ) ) )
16 eqid 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) } = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) }
17 15 16 brabga 
 |-  ( ( X e. B /\ Y e. B ) -> ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) } Y <-> ( ( X e. B /\ Y e. B ) /\ ( .0. .< X /\ A. n e. NN ( n .x. X ) .< Y ) ) ) )
18 17 3adant1 
 |-  ( ( W e. V /\ X e. B /\ Y e. B ) -> ( X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) } Y <-> ( ( X e. B /\ Y e. B ) /\ ( .0. .< X /\ A. n e. NN ( n .x. X ) .< Y ) ) ) )
19 elex 
 |-  ( W e. V -> W e. _V )
20 19 3ad2ant1 
 |-  ( ( W e. V /\ X e. B /\ Y e. B ) -> W e. _V )
21 fveq2 
 |-  ( w = W -> ( Base ` w ) = ( Base ` W ) )
22 21 1 eqtr4di 
 |-  ( w = W -> ( Base ` w ) = B )
23 22 eleq2d 
 |-  ( w = W -> ( x e. ( Base ` w ) <-> x e. B ) )
24 22 eleq2d 
 |-  ( w = W -> ( y e. ( Base ` w ) <-> y e. B ) )
25 23 24 anbi12d 
 |-  ( w = W -> ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) <-> ( x e. B /\ y e. B ) ) )
26 fveq2 
 |-  ( w = W -> ( 0g ` w ) = ( 0g ` W ) )
27 26 2 eqtr4di 
 |-  ( w = W -> ( 0g ` w ) = .0. )
28 fveq2 
 |-  ( w = W -> ( lt ` w ) = ( lt ` W ) )
29 28 4 eqtr4di 
 |-  ( w = W -> ( lt ` w ) = .< )
30 eqidd 
 |-  ( w = W -> x = x )
31 27 29 30 breq123d 
 |-  ( w = W -> ( ( 0g ` w ) ( lt ` w ) x <-> .0. .< x ) )
32 fveq2 
 |-  ( w = W -> ( .g ` w ) = ( .g ` W ) )
33 32 3 eqtr4di 
 |-  ( w = W -> ( .g ` w ) = .x. )
34 33 oveqd 
 |-  ( w = W -> ( n ( .g ` w ) x ) = ( n .x. x ) )
35 eqidd 
 |-  ( w = W -> y = y )
36 34 29 35 breq123d 
 |-  ( w = W -> ( ( n ( .g ` w ) x ) ( lt ` w ) y <-> ( n .x. x ) .< y ) )
37 36 ralbidv 
 |-  ( w = W -> ( A. n e. NN ( n ( .g ` w ) x ) ( lt ` w ) y <-> A. n e. NN ( n .x. x ) .< y ) )
38 31 37 anbi12d 
 |-  ( w = W -> ( ( ( 0g ` w ) ( lt ` w ) x /\ A. n e. NN ( n ( .g ` w ) x ) ( lt ` w ) y ) <-> ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) )
39 25 38 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 ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) ) )
40 39 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 ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) } )
41 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 ) ) } )
42 1 fvexi 
 |-  B e. _V
43 42 42 xpex 
 |-  ( B X. B ) e. _V
44 opabssxp 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) } C_ ( B X. B )
45 43 44 ssexi 
 |-  { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) } e. _V
46 40 41 45 fvmpt 
 |-  ( W e. _V -> ( <<< ` W ) = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) } )
47 20 46 syl 
 |-  ( ( W e. V /\ X e. B /\ Y e. B ) -> ( <<< ` W ) = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) } )
48 47 breqd 
 |-  ( ( W e. V /\ X e. B /\ Y e. B ) -> ( X ( <<< ` W ) Y <-> X { <. x , y >. | ( ( x e. B /\ y e. B ) /\ ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) } Y ) )
49 3simpc 
 |-  ( ( W e. V /\ X e. B /\ Y e. B ) -> ( X e. B /\ Y e. B ) )
50 49 biantrurd 
 |-  ( ( W e. V /\ X e. B /\ Y e. B ) -> ( ( .0. .< X /\ A. n e. NN ( n .x. X ) .< Y ) <-> ( ( X e. B /\ Y e. B ) /\ ( .0. .< X /\ A. n e. NN ( n .x. X ) .< Y ) ) ) )
51 18 48 50 3bitr4d 
 |-  ( ( W e. V /\ X e. B /\ Y e. B ) -> ( X ( <<< ` W ) Y <-> ( .0. .< X /\ A. n e. NN ( n .x. X ) .< Y ) ) )