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 ) )