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 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ) )