Theorem odutos

Description: Being a toset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018)

	Ref	Expression
Hypothesis	odutos.d	⊢ 𝐷 = ( ODual ‘ 𝐾 )
Assertion	odutos	⊢ ( 𝐾 ∈ Toset → 𝐷 ∈ Toset )

Proof

Step	Hyp	Ref	Expression
1		odutos.d	⊢ 𝐷 = ( ODual ‘ 𝐾 )
2		tospos	⊢ ( 𝐾 ∈ Toset → 𝐾 ∈ Poset )
3	1	odupos	⊢ ( 𝐾 ∈ Poset → 𝐷 ∈ Poset )
4	2 3	syl	⊢ ( 𝐾 ∈ Toset → 𝐷 ∈ Poset )
5		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
6		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
7	5 6	tleile	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑦 ( le ‘ 𝐾 ) 𝑥 ∨ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) )
8		vex	⊢ 𝑥 ∈ V
9		vex	⊢ 𝑦 ∈ V
10	8 9	brcnv	⊢ ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ↔ 𝑦 ( le ‘ 𝐾 ) 𝑥 )
11	9 8	brcnv	⊢ ( 𝑦 ◡ ( le ‘ 𝐾 ) 𝑥 ↔ 𝑥 ( le ‘ 𝐾 ) 𝑦 )
12	10 11	orbi12i	⊢ ( ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∨ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑥 ) ↔ ( 𝑦 ( le ‘ 𝐾 ) 𝑥 ∨ 𝑥 ( le ‘ 𝐾 ) 𝑦 ) )
13	7 12	sylibr	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∨ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑥 ) )
14	13	3com23	⊢ ( ( 𝐾 ∈ Toset ∧ 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∨ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑥 ) )
15	14	3expb	⊢ ( ( 𝐾 ∈ Toset ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∨ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑥 ) )
16	15	ralrimivva	⊢ ( 𝐾 ∈ Toset → ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∨ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑥 ) )
17	1 5	odubas	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐷 )
18	1 6	oduleval	⊢ ◡ ( le ‘ 𝐾 ) = ( le ‘ 𝐷 )
19	17 18	istos	⊢ ( 𝐷 ∈ Toset ↔ ( 𝐷 ∈ Poset ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ∀ 𝑦 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ◡ ( le ‘ 𝐾 ) 𝑦 ∨ 𝑦 ◡ ( le ‘ 𝐾 ) 𝑥 ) ) )
20	4 16 19	sylanbrc	⊢ ( 𝐾 ∈ Toset → 𝐷 ∈ Toset )