This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitr3id 
 |-  ( ( <<< ` 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 bitr4di 
 |-  ( ( <<< ` 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 ) )