Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  inftmrel Structured version   Visualization version   Unicode version

Theorem inftmrel 28509
 Description: The infinitesimal relation for a structure . (Contributed by Thierry Arnoux, 30-Jan-2018.)
Hypothesis
Ref Expression
inftm.b
Assertion
Ref Expression
inftmrel <<<

Proof of Theorem inftmrel
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 3056 . . 3
2 fveq2 5870 . . . . . . . . 9
3 inftm.b . . . . . . . . 9
42, 3syl6eqr 2505 . . . . . . . 8
54eleq2d 2516 . . . . . . 7
64eleq2d 2516 . . . . . . 7
75, 6anbi12d 718 . . . . . 6
8 fveq2 5870 . . . . . . . 8
9 fveq2 5870 . . . . . . . 8
10 eqidd 2454 . . . . . . . 8
118, 9, 10breq123d 4419 . . . . . . 7
12 fveq2 5870 . . . . . . . . . 10 .g .g
1312oveqd 6312 . . . . . . . . 9 .g .g
14 eqidd 2454 . . . . . . . . 9
1513, 9, 14breq123d 4419 . . . . . . . 8 .g .g
1615ralbidv 2829 . . . . . . 7 .g .g
1711, 16anbi12d 718 . . . . . 6 .g .g
187, 17anbi12d 718 . . . . 5 .g .g
1918opabbidv 4469 . . . 4 .g .g
20 df-inftm 28507 . . . 4 <<< .g
21 fvex 5880 . . . . . . 7
223, 21eqeltri 2527 . . . . . 6
2322, 22xpex 6600 . . . . 5
24 opabssxp 4912 . . . . 5 .g
2523, 24ssexi 4551 . . . 4 .g
2619, 20, 25fvmpt 5953 . . 3 <<< .g
271, 26syl 17 . 2 <<< .g
2827, 24syl6eqss 3484 1 <<<
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 371   wceq 1446   wcel 1889  wral 2739  cvv 3047   wss 3406   class class class wbr 4405  copab 4463   cxp 4835  cfv 5585  (class class class)co 6295  cn 10616  cbs 15133  c0g 15350  cplt 16198  .gcmg 16684  <<
 Copyright terms: Public domain W3C validator