Metamath Proof Explorer

Theorem odutos

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

Ref Expression
Hypothesis odutos.d ⊢ D = ODual ⁡ K
Assertion odutos ⊢ K ∈ Toset → D ∈ Toset

Proof

Step Hyp Ref Expression
1 odutos.d ⊢ D = ODual ⁡ K
2 tospos ⊢ K ∈ Toset → K ∈ Poset
3 1 odupos ⊢ K ∈ Poset → D ∈ Poset
4 2 3 syl ⊢ K ∈ Toset → D ∈ Poset
5 eqid ⊢ Base K = Base K
6 eqid ⊢ ≤ K = ≤ K
7 5 6 tleile ⊢ K ∈ Toset ∧ y ∈ Base K ∧ x ∈ Base K → y ≤ K x ∨ x ≤ K y
8 vex ⊢ x ∈ V
9 vex ⊢ y ∈ V
10 8 9 brcnv ⊢ x ≤ K -1 y ↔ y ≤ K x
11 9 8 brcnv ⊢ y ≤ K -1 x ↔ x ≤ K y
12 10 11 orbi12i ⊢ x ≤ K -1 y ∨ y ≤ K -1 x ↔ y ≤ K x ∨ x ≤ K y
13 7 12 sylibr ⊢ K ∈ Toset ∧ y ∈ Base K ∧ x ∈ Base K → x ≤ K -1 y ∨ y ≤ K -1 x
14 13 3com23 ⊢ K ∈ Toset ∧ x ∈ Base K ∧ y ∈ Base K → x ≤ K -1 y ∨ y ≤ K -1 x
15 14 3expb ⊢ K ∈ Toset ∧ x ∈ Base K ∧ y ∈ Base K → x ≤ K -1 y ∨ y ≤ K -1 x
16 15 ralrimivva ⊢ K ∈ Toset → ∀ x ∈ Base K ∀ y ∈ Base K x ≤ K -1 y ∨ y ≤ K -1 x
17 1 5 odubas ⊢ Base K = Base D
18 1 6 oduleval ⊢ ≤ K -1 = ≤ D
19 17 18 istos ⊢ D ∈ Toset ↔ D ∈ Poset ∧ ∀ x ∈ Base K ∀ y ∈ Base K x ≤ K -1 y ∨ y ≤ K -1 x
20 4 16 19 sylanbrc ⊢ K ∈ Toset → D ∈ Toset