Metamath Proof Explorer

Theorem isarchi2

Description: Alternative way to express the predicate " W is Archimedean ", for Tosets. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses isarchi2.b 
|- B = ( Base ` W )
isarchi2.0 
|- .0. = ( 0g ` W )
isarchi2.x 
|- .x. = ( .g ` W )
isarchi2.l 
|- .<_ = ( le ` W )
isarchi2.t 
|- .< = ( lt ` W )
Assertion isarchi2 
|- ( ( W e. Toset /\ W e. Mnd ) -> ( W e. Archi <-> A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .<_ ( n .x. x ) ) ) )

Proof

Step Hyp Ref Expression
1 isarchi2.b 
 |-  B = ( Base ` W )
2 isarchi2.0 
 |-  .0. = ( 0g ` W )
3 isarchi2.x 
 |-  .x. = ( .g ` W )
4 isarchi2.l 
 |-  .<_ = ( le ` W )
5 isarchi2.t 
 |-  .< = ( lt ` W )
6 eqid 
 |-  ( <<< ` W ) = ( <<< ` W )
7 1 2 6 isarchi 
 |-  ( W e. Toset -> ( W e. Archi <-> A. x e. B A. y e. B -. x ( <<< ` W ) y ) )
8 7 adantr 
 |-  ( ( W e. Toset /\ W e. Mnd ) -> ( W e. Archi <-> A. x e. B A. y e. B -. x ( <<< ` W ) y ) )
9 simpl1l 
 |-  ( ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) /\ n e. NN ) -> W e. Toset )
10 simpl1r 
 |-  ( ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) /\ n e. NN ) -> W e. Mnd )
11 simpr 
 |-  ( ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) /\ n e. NN ) -> n e. NN )
12 11 nnnn0d 
 |-  ( ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) /\ n e. NN ) -> n e. NN0 )
13 simpl2 
 |-  ( ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) /\ n e. NN ) -> x e. B )
14 1 3 mulgnn0cl 
 |-  ( ( W e. Mnd /\ n e. NN0 /\ x e. B ) -> ( n .x. x ) e. B )
15 10 12 13 14 syl3anc 
 |-  ( ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) /\ n e. NN ) -> ( n .x. x ) e. B )
16 simpl3 
 |-  ( ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) /\ n e. NN ) -> y e. B )
17 1 4 5 tltnle 
 |-  ( ( W e. Toset /\ ( n .x. x ) e. B /\ y e. B ) -> ( ( n .x. x ) .< y <-> -. y .<_ ( n .x. x ) ) )
18 17 con2bid 
 |-  ( ( W e. Toset /\ ( n .x. x ) e. B /\ y e. B ) -> ( y .<_ ( n .x. x ) <-> -. ( n .x. x ) .< y ) )
19 9 15 16 18 syl3anc 
 |-  ( ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) /\ n e. NN ) -> ( y .<_ ( n .x. x ) <-> -. ( n .x. x ) .< y ) )
20 19 rexbidva 
 |-  ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) -> ( E. n e. NN y .<_ ( n .x. x ) <-> E. n e. NN -. ( n .x. x ) .< y ) )
21 20 imbi2d 
 |-  ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) -> ( ( .0. .< x -> E. n e. NN y .<_ ( n .x. x ) ) <-> ( .0. .< x -> E. n e. NN -. ( n .x. x ) .< y ) ) )
22 1 2 3 5 isinftm 
 |-  ( ( W e. Toset /\ x e. B /\ y e. B ) -> ( x ( <<< ` W ) y <-> ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) )
23 22 notbid 
 |-  ( ( W e. Toset /\ x e. B /\ y e. B ) -> ( -. x ( <<< ` W ) y <-> -. ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) ) )
24 rexnal 
 |-  ( E. n e. NN -. ( n .x. x ) .< y <-> -. A. n e. NN ( n .x. x ) .< y )
25 24 imbi2i 
 |-  ( ( .0. .< x -> E. n e. NN -. ( n .x. x ) .< y ) <-> ( .0. .< x -> -. A. n e. NN ( n .x. x ) .< y ) )
26 imnan 
 |-  ( ( .0. .< x -> -. A. n e. NN ( n .x. x ) .< y ) <-> -. ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) )
27 25 26 bitr2i 
 |-  ( -. ( .0. .< x /\ A. n e. NN ( n .x. x ) .< y ) <-> ( .0. .< x -> E. n e. NN -. ( n .x. x ) .< y ) )
28 23 27 bitrdi 
 |-  ( ( W e. Toset /\ x e. B /\ y e. B ) -> ( -. x ( <<< ` W ) y <-> ( .0. .< x -> E. n e. NN -. ( n .x. x ) .< y ) ) )
29 28 3adant1r 
 |-  ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) -> ( -. x ( <<< ` W ) y <-> ( .0. .< x -> E. n e. NN -. ( n .x. x ) .< y ) ) )
30 21 29 bitr4d 
 |-  ( ( ( W e. Toset /\ W e. Mnd ) /\ x e. B /\ y e. B ) -> ( ( .0. .< x -> E. n e. NN y .<_ ( n .x. x ) ) <-> -. x ( <<< ` W ) y ) )
31 30 3expb 
 |-  ( ( ( W e. Toset /\ W e. Mnd ) /\ ( x e. B /\ y e. B ) ) -> ( ( .0. .< x -> E. n e. NN y .<_ ( n .x. x ) ) <-> -. x ( <<< ` W ) y ) )
32 31 2ralbidva 
 |-  ( ( W e. Toset /\ W e. Mnd ) -> ( A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .<_ ( n .x. x ) ) <-> A. x e. B A. y e. B -. x ( <<< ` W ) y ) )
33 8 32 bitr4d 
 |-  ( ( W e. Toset /\ W e. Mnd ) -> ( W e. Archi <-> A. x e. B A. y e. B ( .0. .< x -> E. n e. NN y .<_ ( n .x. x ) ) ) )