Metamath Proof Explorer


Theorem isarchi

Description: Express the predicate " W is Archimedean ". (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Hypotheses isarchi.b 𝐵 = ( Base ‘ 𝑊 )
isarchi.0 0 = ( 0g𝑊 )
isarchi.i < = ( ⋘ ‘ 𝑊 )
Assertion isarchi ( 𝑊𝑉 → ( 𝑊 ∈ Archi ↔ ∀ 𝑥𝐵𝑦𝐵 ¬ 𝑥 < 𝑦 ) )

Proof

Step Hyp Ref Expression
1 isarchi.b 𝐵 = ( Base ‘ 𝑊 )
2 isarchi.0 0 = ( 0g𝑊 )
3 isarchi.i < = ( ⋘ ‘ 𝑊 )
4 fveqeq2 ( 𝑤 = 𝑊 → ( ( ⋘ ‘ 𝑤 ) = ∅ ↔ ( ⋘ ‘ 𝑊 ) = ∅ ) )
5 df-archi Archi = { 𝑤 ∣ ( ⋘ ‘ 𝑤 ) = ∅ }
6 4 5 elab2g ( 𝑊𝑉 → ( 𝑊 ∈ Archi ↔ ( ⋘ ‘ 𝑊 ) = ∅ ) )
7 1 inftmrel ( 𝑊𝑉 → ( ⋘ ‘ 𝑊 ) ⊆ ( 𝐵 × 𝐵 ) )
8 ss0b ( ( ⋘ ‘ 𝑊 ) ⊆ ∅ ↔ ( ⋘ ‘ 𝑊 ) = ∅ )
9 ssrel2 ( ( ⋘ ‘ 𝑊 ) ⊆ ( 𝐵 × 𝐵 ) → ( ( ⋘ ‘ 𝑊 ) ⊆ ∅ ↔ ∀ 𝑥𝐵𝑦𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) ) )
10 8 9 bitr3id ( ( ⋘ ‘ 𝑊 ) ⊆ ( 𝐵 × 𝐵 ) → ( ( ⋘ ‘ 𝑊 ) = ∅ ↔ ∀ 𝑥𝐵𝑦𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) ) )
11 noel ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅
12 11 nbn ( ¬ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
13 3 breqi ( 𝑥 < 𝑦𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 )
14 df-br ( 𝑥 ( ⋘ ‘ 𝑊 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) )
15 13 14 bitri ( 𝑥 < 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) )
16 12 15 xchnxbir ( ¬ 𝑥 < 𝑦 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
17 11 pm2.21i ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) )
18 dfbi2 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) ↔ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) ) ) )
19 17 18 mpbiran2 ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
20 16 19 bitri ( ¬ 𝑥 < 𝑦 ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
21 20 2ralbii ( ∀ 𝑥𝐵𝑦𝐵 ¬ 𝑥 < 𝑦 ↔ ∀ 𝑥𝐵𝑦𝐵 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ⋘ ‘ 𝑊 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∅ ) )
22 10 21 bitr4di ( ( ⋘ ‘ 𝑊 ) ⊆ ( 𝐵 × 𝐵 ) → ( ( ⋘ ‘ 𝑊 ) = ∅ ↔ ∀ 𝑥𝐵𝑦𝐵 ¬ 𝑥 < 𝑦 ) )
23 7 22 syl ( 𝑊𝑉 → ( ( ⋘ ‘ 𝑊 ) = ∅ ↔ ∀ 𝑥𝐵𝑦𝐵 ¬ 𝑥 < 𝑦 ) )
24 6 23 bitrd ( 𝑊𝑉 → ( 𝑊 ∈ Archi ↔ ∀ 𝑥𝐵𝑦𝐵 ¬ 𝑥 < 𝑦 ) )