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 ˙ = 0 W
isarchi.i < ˙ = W
Assertion isarchi W V W Archi x B y B ¬ x < ˙ y

Proof

Step Hyp Ref Expression
1 isarchi.b B = Base W
2 isarchi.0 0 ˙ = 0 W
3 isarchi.i < ˙ = W
4 fveqeq2 w = W w = W =
5 df-archi Archi = w | w =
6 4 5 elab2g W V W Archi W =
7 1 inftmrel W V W B × B
8 ss0b W W =
9 ssrel2 W B × B W x B y B x y W x y
10 8 9 bitr3id W B × B W = x B y B x y W x y
11 noel ¬ x y
12 11 nbn ¬ x y W x y W x y
13 3 breqi x < ˙ y x W y
14 df-br x W y x y W
15 13 14 bitri x < ˙ y x y W
16 12 15 xchnxbir ¬ x < ˙ y x y W x y
17 11 pm2.21i x y x y W
18 dfbi2 x y W x y x y W x y x y x y W
19 17 18 mpbiran2 x y W x y x y W x y
20 16 19 bitri ¬ x < ˙ y x y W x y
21 20 2ralbii x B y B ¬ x < ˙ y x B y B x y W x y
22 10 21 bitr4di W B × B W = x B y B ¬ x < ˙ y
23 7 22 syl W V W = x B y B ¬ x < ˙ y
24 6 23 bitrd W V W Archi x B y B ¬ x < ˙ y