Step |
Hyp |
Ref |
Expression |
1 |
|
istos.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
istos.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
fveq2 |
⊢ ( 𝑓 = 𝐾 → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐾 ) ) |
4 |
|
fveq2 |
⊢ ( 𝑓 = 𝐾 → ( le ‘ 𝑓 ) = ( le ‘ 𝐾 ) ) |
5 |
4
|
sbceq1d |
⊢ ( 𝑓 = 𝐾 → ( [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ [ ( le ‘ 𝐾 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ) ) |
6 |
3 5
|
sbceqbid |
⊢ ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ [ ( Base ‘ 𝐾 ) / 𝑏 ] [ ( le ‘ 𝐾 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ) ) |
7 |
|
fvex |
⊢ ( Base ‘ 𝐾 ) ∈ V |
8 |
|
fvex |
⊢ ( le ‘ 𝐾 ) ∈ V |
9 |
|
eqtr |
⊢ ( ( 𝑏 = ( Base ‘ 𝐾 ) ∧ ( Base ‘ 𝐾 ) = 𝐵 ) → 𝑏 = 𝐵 ) |
10 |
|
eqtr |
⊢ ( ( 𝑟 = ( le ‘ 𝐾 ) ∧ ( le ‘ 𝐾 ) = ≤ ) → 𝑟 = ≤ ) |
11 |
|
breq |
⊢ ( 𝑟 = ≤ → ( 𝑥 𝑟 𝑦 ↔ 𝑥 ≤ 𝑦 ) ) |
12 |
|
breq |
⊢ ( 𝑟 = ≤ → ( 𝑦 𝑟 𝑥 ↔ 𝑦 ≤ 𝑥 ) ) |
13 |
11 12
|
orbi12d |
⊢ ( 𝑟 = ≤ → ( ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) |
14 |
13
|
2ralbidv |
⊢ ( 𝑟 = ≤ → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) |
15 |
|
raleq |
⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑦 ∈ 𝑏 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) |
16 |
15
|
raleqbi1dv |
⊢ ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) |
17 |
14 16
|
sylan9bb |
⊢ ( ( 𝑟 = ≤ ∧ 𝑏 = 𝐵 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) |
18 |
17
|
ex |
⊢ ( 𝑟 = ≤ → ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) ) |
19 |
10 18
|
syl |
⊢ ( ( 𝑟 = ( le ‘ 𝐾 ) ∧ ( le ‘ 𝐾 ) = ≤ ) → ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) ) |
20 |
19
|
expcom |
⊢ ( ( le ‘ 𝐾 ) = ≤ → ( 𝑟 = ( le ‘ 𝐾 ) → ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) ) ) |
21 |
20
|
eqcoms |
⊢ ( ≤ = ( le ‘ 𝐾 ) → ( 𝑟 = ( le ‘ 𝐾 ) → ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) ) ) |
22 |
2 21
|
ax-mp |
⊢ ( 𝑟 = ( le ‘ 𝐾 ) → ( 𝑏 = 𝐵 → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) ) |
23 |
9 22
|
syl5com |
⊢ ( ( 𝑏 = ( Base ‘ 𝐾 ) ∧ ( Base ‘ 𝐾 ) = 𝐵 ) → ( 𝑟 = ( le ‘ 𝐾 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) ) |
24 |
23
|
expcom |
⊢ ( ( Base ‘ 𝐾 ) = 𝐵 → ( 𝑏 = ( Base ‘ 𝐾 ) → ( 𝑟 = ( le ‘ 𝐾 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) ) ) |
25 |
24
|
eqcoms |
⊢ ( 𝐵 = ( Base ‘ 𝐾 ) → ( 𝑏 = ( Base ‘ 𝐾 ) → ( 𝑟 = ( le ‘ 𝐾 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) ) ) |
26 |
1 25
|
ax-mp |
⊢ ( 𝑏 = ( Base ‘ 𝐾 ) → ( 𝑟 = ( le ‘ 𝐾 ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) ) |
27 |
26
|
imp |
⊢ ( ( 𝑏 = ( Base ‘ 𝐾 ) ∧ 𝑟 = ( le ‘ 𝐾 ) ) → ( ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) |
28 |
7 8 27
|
sbc2ie |
⊢ ( [ ( Base ‘ 𝐾 ) / 𝑏 ] [ ( le ‘ 𝐾 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) |
29 |
6 28
|
bitrdi |
⊢ ( 𝑓 = 𝐾 → ( [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) |
30 |
|
df-toset |
⊢ Toset = { 𝑓 ∈ Poset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ( 𝑥 𝑟 𝑦 ∨ 𝑦 𝑟 𝑥 ) } |
31 |
29 30
|
elrab2 |
⊢ ( 𝐾 ∈ Toset ↔ ( 𝐾 ∈ Poset ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) ) |