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