# 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}={\mathrm{Base}}_{{W}}$
isarchi.0
isarchi.i
Assertion isarchi

### Proof

Step Hyp Ref Expression
1 isarchi.b ${⊢}{B}={\mathrm{Base}}_{{W}}$
2 isarchi.0
3 isarchi.i
4 fveqeq2 ${⊢}{w}={W}\to \left(⋘\left({w}\right)=\varnothing ↔⋘\left({W}\right)=\varnothing \right)$
5 df-archi ${⊢}\mathrm{Archi}=\left\{{w}|⋘\left({w}\right)=\varnothing \right\}$
6 4 5 elab2g ${⊢}{W}\in {V}\to \left({W}\in \mathrm{Archi}↔⋘\left({W}\right)=\varnothing \right)$
7 1 inftmrel ${⊢}{W}\in {V}\to ⋘\left({W}\right)\subseteq {B}×{B}$
8 ss0b ${⊢}⋘\left({W}\right)\subseteq \varnothing ↔⋘\left({W}\right)=\varnothing$
9 ssrel2 ${⊢}⋘\left({W}\right)\subseteq {B}×{B}\to \left(⋘\left({W}\right)\subseteq \varnothing ↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in ⋘\left({W}\right)\to ⟨{x},{y}⟩\in \varnothing \right)\right)$
10 8 9 syl5bbr ${⊢}⋘\left({W}\right)\subseteq {B}×{B}\to \left(⋘\left({W}\right)=\varnothing ↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\forall {y}\in {B}\phantom{\rule{.4em}{0ex}}\left(⟨{x},{y}⟩\in ⋘\left({W}\right)\to ⟨{x},{y}⟩\in \varnothing \right)\right)$
11 noel ${⊢}¬⟨{x},{y}⟩\in \varnothing$
12 11 nbn ${⊢}¬⟨{x},{y}⟩\in ⋘\left({W}\right)↔\left(⟨{x},{y}⟩\in ⋘\left({W}\right)↔⟨{x},{y}⟩\in \varnothing \right)$
13 3 breqi
14 df-br ${⊢}{x}⋘\left({W}\right){y}↔⟨{x},{y}⟩\in ⋘\left({W}\right)$
15 13 14 bitri
16 12 15 xchnxbir
17 11 pm2.21i ${⊢}⟨{x},{y}⟩\in \varnothing \to ⟨{x},{y}⟩\in ⋘\left({W}\right)$
18 dfbi2 ${⊢}\left(⟨{x},{y}⟩\in ⋘\left({W}\right)↔⟨{x},{y}⟩\in \varnothing \right)↔\left(\left(⟨{x},{y}⟩\in ⋘\left({W}\right)\to ⟨{x},{y}⟩\in \varnothing \right)\wedge \left(⟨{x},{y}⟩\in \varnothing \to ⟨{x},{y}⟩\in ⋘\left({W}\right)\right)\right)$
19 17 18 mpbiran2 ${⊢}\left(⟨{x},{y}⟩\in ⋘\left({W}\right)↔⟨{x},{y}⟩\in \varnothing \right)↔\left(⟨{x},{y}⟩\in ⋘\left({W}\right)\to ⟨{x},{y}⟩\in \varnothing \right)$
20 16 19 bitri
21 20 2ralbii
22 10 21 syl6bbr
23 7 22 syl
24 6 23 bitrd