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	$$⊢\underset{\dot{}}{0}=0_W$$
	isarchi.i	$$⊢\underset{\dot{}}{<}=⋘\left(W\right)$$
Assertion	isarchi	$$⊢W\in V\to \left(W\in \mathrm{Archi}\leftrightarrow \forall x\in B\forall y\in B\neg x\underset{\dot{}}{<}y\right)$$

Proof

Step	Hyp	Ref	Expression
1		isarchi.b	$$⊢B={\mathrm{Base}}_W$$
2		isarchi.0	$$⊢\underset{\dot{}}{0}=0_W$$
3		isarchi.i	$$⊢\underset{\dot{}}{<}=⋘\left(W\right)$$
4		fveqeq2	$$⊢w=W\to \left(⋘\left(w\right)=\varnothing \leftrightarrow ⋘\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}\leftrightarrow ⋘\left(W\right)=\varnothing \right)$$
7	1	inftmrel	$$⊢W\in V\to ⋘\left(W\right)\subseteq B\times B$$
8		ss0b	$$⊢⋘\left(W\right)\subseteq \varnothing \leftrightarrow ⋘\left(W\right)=\varnothing$$
9		ssrel2	$$⊢⋘\left(W\right)\subseteq B\times B\to \left(⋘\left(W\right)\subseteq \varnothing \leftrightarrow \forall x\in B\forall y\in B\left(⟨x,y⟩\in ⋘\left(W\right)\to ⟨x,y⟩\in \varnothing \right)\right)$$
10	8 9	bitr3id	$$⊢⋘\left(W\right)\subseteq B\times B\to \left(⋘\left(W\right)=\varnothing \leftrightarrow \forall x\in B\forall y\in B\left(⟨x,y⟩\in ⋘\left(W\right)\to ⟨x,y⟩\in \varnothing \right)\right)$$
11		noel	$$⊢\neg ⟨x,y⟩\in \varnothing$$
12	11	nbn	$$⊢\neg ⟨x,y⟩\in ⋘\left(W\right)\leftrightarrow \left(⟨x,y⟩\in ⋘\left(W\right)\leftrightarrow ⟨x,y⟩\in \varnothing \right)$$
13	3	breqi	$$⊢x\underset{\dot{}}{<}y\leftrightarrow x⋘\left(W\right)y$$
14		df-br	$$⊢x⋘\left(W\right)y\leftrightarrow ⟨x,y⟩\in ⋘\left(W\right)$$
15	13 14	bitri	$$⊢x\underset{\dot{}}{<}y\leftrightarrow ⟨x,y⟩\in ⋘\left(W\right)$$
16	12 15	xchnxbir	$$⊢\neg x\underset{\dot{}}{<}y\leftrightarrow \left(⟨x,y⟩\in ⋘\left(W\right)\leftrightarrow ⟨x,y⟩\in \varnothing \right)$$
17	11	pm2.21i	$$⊢⟨x,y⟩\in \varnothing \to ⟨x,y⟩\in ⋘\left(W\right)$$
18		dfbi2	$$⊢\left(⟨x,y⟩\in ⋘\left(W\right)\leftrightarrow ⟨x,y⟩\in \varnothing \right)\leftrightarrow \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)\leftrightarrow ⟨x,y⟩\in \varnothing \right)\leftrightarrow \left(⟨x,y⟩\in ⋘\left(W\right)\to ⟨x,y⟩\in \varnothing \right)$$
20	16 19	bitri	$$⊢\neg x\underset{\dot{}}{<}y\leftrightarrow \left(⟨x,y⟩\in ⋘\left(W\right)\to ⟨x,y⟩\in \varnothing \right)$$
21	20	2ralbii	$$⊢\forall x\in B\forall y\in B\neg x\underset{\dot{}}{<}y\leftrightarrow \forall x\in B\forall y\in B\left(⟨x,y⟩\in ⋘\left(W\right)\to ⟨x,y⟩\in \varnothing \right)$$
22	10 21	bitr4di	$$⊢⋘\left(W\right)\subseteq B\times B\to \left(⋘\left(W\right)=\varnothing \leftrightarrow \forall x\in B\forall y\in B\neg x\underset{\dot{}}{<}y\right)$$
23	7 22	syl	$$⊢W\in V\to \left(⋘\left(W\right)=\varnothing \leftrightarrow \forall x\in B\forall y\in B\neg x\underset{\dot{}}{<}y\right)$$
24	6 23	bitrd	$$⊢W\in V\to \left(W\in \mathrm{Archi}\leftrightarrow \forall x\in B\forall y\in B\neg x\underset{\dot{}}{<}y\right)$$