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

Theorem isarchi 26150
 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 elex 2976 . . 3
2 fveq2 5686 . . . . . 6 <<< <<<
32eqeq1d 2446 . . . . 5 <<< <<<
4 df-archi 26147 . . . . 5 Archi <<<
53, 4elrab2 3114 . . . 4 Archi <<<
65baib 896 . . 3 Archi <<<
71, 6syl 16 . 2 Archi <<<
8 isarchi.b . . . 4
98inftmrel 26148 . . 3 <<<
10 ss0b 3662 . . . . 5 <<< <<<
11 ssrel2 4925 . . . . 5 <<< <<< <<<
1210, 11syl5bbr 259 . . . 4 <<< <<< <<<
13 noel 3636 . . . . . . . 8
1413nbn 347 . . . . . . 7 <<< <<<
15 isarchi.i . . . . . . . . 9 <<<
1615breqi 4293 . . . . . . . 8 <<<
17 df-br 4288 . . . . . . . 8 <<< <<<
1816, 17bitri 249 . . . . . . 7 <<<
1914, 18xchnxbir 309 . . . . . 6 <<<
2013pm2.21i 131 . . . . . . 7 <<<
21 dfbi2 628 . . . . . . 7 <<< <<< <<<
2220, 21mpbiran2 910 . . . . . 6 <<< <<<
2319, 22bitri 249 . . . . 5 <<<
24232ralbii 2736 . . . 4 <<<
2512, 24syl6bbr 263 . . 3 <<< <<<
269, 25syl 16 . 2 <<<
277, 26bitrd 253 1 Archi
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wceq 1369   wcel 1756  wral 2710  cvv 2967   wss 3323  c0 3632  cop 3878   class class class wbr 4287   cxp 4833  cfv 5413  cbs 14166  c0g 14370  <<
 Copyright terms: Public domain W3C validator