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

Theorem isarchi 28506
 Description: Express the predicate " is Archimedean ". (Contributed by Thierry Arnoux, 30-Jan-2018.)
Hypotheses
Ref Expression
isarchi.b
isarchi.0
isarchi.i <<<
Assertion
Ref Expression
isarchi Archi
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)

Proof of Theorem isarchi
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fveq2 5881 . . . 4 <<< <<<
21eqeq1d 2424 . . 3 <<< <<<
3 df-archi 28503 . . 3 Archi <<<
42, 3elab2g 3219 . 2 Archi <<<
5 isarchi.b . . . 4
65inftmrel 28504 . . 3 <<<
7 ss0b 3794 . . . . 5 <<< <<<
8 ssrel2 4944 . . . . 5 <<< <<< <<<
97, 8syl5bbr 262 . . . 4 <<< <<< <<<
10 noel 3765 . . . . . . . 8
1110nbn 348 . . . . . . 7 <<< <<<
12 isarchi.i . . . . . . . . 9 <<<
1312breqi 4429 . . . . . . . 8 <<<
14 df-br 4424 . . . . . . . 8 <<< <<<
1513, 14bitri 252 . . . . . . 7 <<<
1611, 15xchnxbir 310 . . . . . 6 <<<
1710pm2.21i 134 . . . . . . 7 <<<
18 dfbi2 632 . . . . . . 7 <<< <<< <<<
1917, 18mpbiran2 927 . . . . . 6 <<< <<<
2016, 19bitri 252 . . . . 5 <<<
21202ralbii 2854 . . . 4 <<<
229, 21syl6bbr 266 . . 3 <<< <<<
236, 22syl 17 . 2 <<<
244, 23bitrd 256 1 Archi
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wceq 1437   wcel 1872  wral 2771   wss 3436  c0 3761  cop 4004   class class class wbr 4423   cxp 4851  cfv 5601  cbs 15120  c0g 15337  <<
 Copyright terms: Public domain W3C validator