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 𝐷 = ( 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 )