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 ) |