# Metamath Proof Explorer

## Theorem isarchi

Description: Express the predicate " W is Archimedean ". (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses isarchi.b
`|- B = ( Base ` W )`
isarchi.0
`|- .0. = ( 0g ` W )`
isarchi.i
`|- .< = ( <<< ` W )`
Assertion isarchi
`|- ( W e. V -> ( W e. Archi <-> A. x e. B A. y e. B -. x .< y ) )`

### Proof

Step Hyp Ref Expression
1 isarchi.b
` |-  B = ( Base ` W )`
2 isarchi.0
` |-  .0. = ( 0g ` W )`
3 isarchi.i
` |-  .< = ( <<< ` W )`
4 fveqeq2
` |-  ( w = W -> ( ( <<< ` w ) = (/) <-> ( <<< ` W ) = (/) ) )`
5 df-archi
` |-  Archi = { w | ( <<< ` w ) = (/) }`
6 4 5 elab2g
` |-  ( W e. V -> ( W e. Archi <-> ( <<< ` W ) = (/) ) )`
7 1 inftmrel
` |-  ( W e. V -> ( <<< ` W ) C_ ( B X. B ) )`
8 ss0b
` |-  ( ( <<< ` W ) C_ (/) <-> ( <<< ` W ) = (/) )`
9 ssrel2
` |-  ( ( <<< ` W ) C_ ( B X. B ) -> ( ( <<< ` W ) C_ (/) <-> A. x e. B A. y e. B ( <. x , y >. e. ( <<< ` W ) -> <. x , y >. e. (/) ) ) )`
10 8 9 syl5bbr
` |-  ( ( <<< ` W ) C_ ( B X. B ) -> ( ( <<< ` W ) = (/) <-> A. x e. B A. y e. B ( <. x , y >. e. ( <<< ` W ) -> <. x , y >. e. (/) ) ) )`
11 noel
` |-  -. <. x , y >. e. (/)`
12 11 nbn
` |-  ( -. <. x , y >. e. ( <<< ` W ) <-> ( <. x , y >. e. ( <<< ` W ) <-> <. x , y >. e. (/) ) )`
13 3 breqi
` |-  ( x .< y <-> x ( <<< ` W ) y )`
14 df-br
` |-  ( x ( <<< ` W ) y <-> <. x , y >. e. ( <<< ` W ) )`
15 13 14 bitri
` |-  ( x .< y <-> <. x , y >. e. ( <<< ` W ) )`
16 12 15 xchnxbir
` |-  ( -. x .< y <-> ( <. x , y >. e. ( <<< ` W ) <-> <. x , y >. e. (/) ) )`
17 11 pm2.21i
` |-  ( <. x , y >. e. (/) -> <. x , y >. e. ( <<< ` W ) )`
18 dfbi2
` |-  ( ( <. x , y >. e. ( <<< ` W ) <-> <. x , y >. e. (/) ) <-> ( ( <. x , y >. e. ( <<< ` W ) -> <. x , y >. e. (/) ) /\ ( <. x , y >. e. (/) -> <. x , y >. e. ( <<< ` W ) ) ) )`
19 17 18 mpbiran2
` |-  ( ( <. x , y >. e. ( <<< ` W ) <-> <. x , y >. e. (/) ) <-> ( <. x , y >. e. ( <<< ` W ) -> <. x , y >. e. (/) ) )`
20 16 19 bitri
` |-  ( -. x .< y <-> ( <. x , y >. e. ( <<< ` W ) -> <. x , y >. e. (/) ) )`
21 20 2ralbii
` |-  ( A. x e. B A. y e. B -. x .< y <-> A. x e. B A. y e. B ( <. x , y >. e. ( <<< ` W ) -> <. x , y >. e. (/) ) )`
22 10 21 syl6bbr
` |-  ( ( <<< ` W ) C_ ( B X. B ) -> ( ( <<< ` W ) = (/) <-> A. x e. B A. y e. B -. x .< y ) )`
23 7 22 syl
` |-  ( W e. V -> ( ( <<< ` W ) = (/) <-> A. x e. B A. y e. B -. x .< y ) )`
24 6 23 bitrd
` |-  ( W e. V -> ( W e. Archi <-> A. x e. B A. y e. B -. x .< y ) )`