Step | Hyp | Ref
| Expression |
1 | | pospo.s |
. . . . 5
⊢ < =
(lt‘𝐾) |
2 | 1 | pltirr 17572 |
. . . 4
⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵) → ¬ 𝑥 < 𝑥) |
3 | | pospo.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
4 | 3, 1 | plttr 17579 |
. . . 4
⊢ ((𝐾 ∈ Poset ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧)) |
5 | 2, 4 | ispod 5481 |
. . 3
⊢ (𝐾 ∈ Poset → < Po 𝐵) |
6 | | relres 5881 |
. . . . 5
⊢ Rel ( I
↾ 𝐵) |
7 | 6 | a1i 11 |
. . . 4
⊢ (𝐾 ∈ Poset → Rel ( I
↾ 𝐵)) |
8 | | opabresid 5916 |
. . . . . . . 8
⊢ ( I
↾ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥)} |
9 | 8 | eqcomi 2830 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥)} = ( I ↾ 𝐵) |
10 | 9 | eleq2i 2904 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥)} ↔ 〈𝑥, 𝑦〉 ∈ ( I ↾ 𝐵)) |
11 | | opabidw 5411 |
. . . . . 6
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥)} ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥)) |
12 | 10, 11 | bitr3i 279 |
. . . . 5
⊢
(〈𝑥, 𝑦〉 ∈ ( I ↾ 𝐵) ↔ (𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥)) |
13 | | pospo.l |
. . . . . . . 8
⊢ ≤ =
(le‘𝐾) |
14 | 3, 13 | posref 17560 |
. . . . . . 7
⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥) |
15 | | df-br 5066 |
. . . . . . . 8
⊢ (𝑥 ≤ 𝑦 ↔ 〈𝑥, 𝑦〉 ∈ ≤ ) |
16 | | breq2 5069 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑥 ≤ 𝑦 ↔ 𝑥 ≤ 𝑥)) |
17 | 15, 16 | syl5bbr 287 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (〈𝑥, 𝑦〉 ∈ ≤ ↔ 𝑥 ≤ 𝑥)) |
18 | 14, 17 | syl5ibrcom 249 |
. . . . . 6
⊢ ((𝐾 ∈ Poset ∧ 𝑥 ∈ 𝐵) → (𝑦 = 𝑥 → 〈𝑥, 𝑦〉 ∈ ≤ )) |
19 | 18 | expimpd 456 |
. . . . 5
⊢ (𝐾 ∈ Poset → ((𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥) → 〈𝑥, 𝑦〉 ∈ ≤ )) |
20 | 12, 19 | syl5bi 244 |
. . . 4
⊢ (𝐾 ∈ Poset →
(〈𝑥, 𝑦〉 ∈ ( I ↾ 𝐵) → 〈𝑥, 𝑦〉 ∈ ≤ )) |
21 | 7, 20 | relssdv 5660 |
. . 3
⊢ (𝐾 ∈ Poset → ( I ↾
𝐵) ⊆ ≤
) |
22 | 5, 21 | jca 514 |
. 2
⊢ (𝐾 ∈ Poset → ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) |
23 | | elex 3512 |
. . . . 5
⊢ (𝐾 ∈ 𝑉 → 𝐾 ∈ V) |
24 | 23 | adantr 483 |
. . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) → 𝐾 ∈ V) |
25 | 3 | a1i 11 |
. . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) → 𝐵 = (Base‘𝐾)) |
26 | 13 | a1i 11 |
. . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) → ≤ =
(le‘𝐾)) |
27 | | equid 2015 |
. . . . . 6
⊢ 𝑥 = 𝑥 |
28 | | simpr 487 |
. . . . . . 7
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
29 | | resieq 5863 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑥( I ↾ 𝐵)𝑥 ↔ 𝑥 = 𝑥)) |
30 | 28, 28, 29 | syl2anc 586 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵) → (𝑥( I ↾ 𝐵)𝑥 ↔ 𝑥 = 𝑥)) |
31 | 27, 30 | mpbiri 260 |
. . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵) → 𝑥( I ↾ 𝐵)𝑥) |
32 | | simplrr 776 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵) → ( I ↾ 𝐵) ⊆ ≤ ) |
33 | 32 | ssbrd 5108 |
. . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵) → (𝑥( I ↾ 𝐵)𝑥 → 𝑥 ≤ 𝑥)) |
34 | 31, 33 | mpd 15 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥) |
35 | 3, 13, 1 | pleval2i 17573 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ≤ 𝑦 → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))) |
36 | 35 | 3adant1 1126 |
. . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ≤ 𝑦 → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))) |
37 | 3, 13, 1 | pleval2i 17573 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝑦 ≤ 𝑥 → (𝑦 < 𝑥 ∨ 𝑦 = 𝑥))) |
38 | 37 | ancoms 461 |
. . . . . 6
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑦 ≤ 𝑥 → (𝑦 < 𝑥 ∨ 𝑦 = 𝑥))) |
39 | 38 | 3adant1 1126 |
. . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑦 ≤ 𝑥 → (𝑦 < 𝑥 ∨ 𝑦 = 𝑥))) |
40 | | simprl 769 |
. . . . . . . 8
⊢ ((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) → < Po 𝐵) |
41 | | po2nr 5486 |
. . . . . . . . 9
⊢ (( < Po 𝐵 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ¬ (𝑥 < 𝑦 ∧ 𝑦 < 𝑥)) |
42 | 41 | 3impb 1111 |
. . . . . . . 8
⊢ (( < Po 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ¬ (𝑥 < 𝑦 ∧ 𝑦 < 𝑥)) |
43 | 40, 42 | syl3an1 1159 |
. . . . . . 7
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ¬ (𝑥 < 𝑦 ∧ 𝑦 < 𝑥)) |
44 | 43 | pm2.21d 121 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑥) → 𝑥 = 𝑦)) |
45 | | simpl 485 |
. . . . . . 7
⊢ ((𝑥 = 𝑦 ∧ 𝑦 < 𝑥) → 𝑥 = 𝑦) |
46 | 45 | a1i 11 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 = 𝑦 ∧ 𝑦 < 𝑥) → 𝑥 = 𝑦)) |
47 | | simpr 487 |
. . . . . . . 8
⊢ ((𝑥 < 𝑦 ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥) |
48 | 47 | equcomd 2022 |
. . . . . . 7
⊢ ((𝑥 < 𝑦 ∧ 𝑦 = 𝑥) → 𝑥 = 𝑦) |
49 | 48 | a1i 11 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 < 𝑦 ∧ 𝑦 = 𝑥) → 𝑥 = 𝑦)) |
50 | | simpl 485 |
. . . . . . 7
⊢ ((𝑥 = 𝑦 ∧ 𝑦 = 𝑥) → 𝑥 = 𝑦) |
51 | 50 | a1i 11 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 = 𝑦 ∧ 𝑦 = 𝑥) → 𝑥 = 𝑦)) |
52 | 44, 46, 49, 51 | ccased 1033 |
. . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (((𝑥 < 𝑦 ∨ 𝑥 = 𝑦) ∧ (𝑦 < 𝑥 ∨ 𝑦 = 𝑥)) → 𝑥 = 𝑦)) |
53 | 36, 39, 52 | syl2and 609 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) |
54 | | simpr1 1190 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
55 | | simpr2 1191 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
56 | 54, 55, 35 | syl2anc 586 |
. . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 ≤ 𝑦 → (𝑥 < 𝑦 ∨ 𝑥 = 𝑦))) |
57 | | simpr3 1192 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑧 ∈ 𝐵) |
58 | 3, 13, 1 | pleval2i 17573 |
. . . . . 6
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦 ≤ 𝑧 → (𝑦 < 𝑧 ∨ 𝑦 = 𝑧))) |
59 | 55, 57, 58 | syl2anc 586 |
. . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦 ≤ 𝑧 → (𝑦 < 𝑧 ∨ 𝑦 = 𝑧))) |
60 | | potr 5485 |
. . . . . . . 8
⊢ (( < Po 𝐵 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧)) |
61 | 40, 60 | sylan 582 |
. . . . . . 7
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧)) |
62 | | simpll 765 |
. . . . . . . 8
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝐾 ∈ 𝑉) |
63 | 13, 1 | pltle 17570 |
. . . . . . . 8
⊢ ((𝐾 ∈ 𝑉 ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑥 < 𝑧 → 𝑥 ≤ 𝑧)) |
64 | 62, 54, 57, 63 | syl3anc 1367 |
. . . . . . 7
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 < 𝑧 → 𝑥 ≤ 𝑧)) |
65 | 61, 64 | syld 47 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 < 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 ≤ 𝑧)) |
66 | | breq1 5068 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑥 < 𝑧 ↔ 𝑦 < 𝑧)) |
67 | 66 | biimpar 480 |
. . . . . . 7
⊢ ((𝑥 = 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 < 𝑧) |
68 | 67, 64 | syl5 34 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 = 𝑦 ∧ 𝑦 < 𝑧) → 𝑥 ≤ 𝑧)) |
69 | | breq2 5069 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝑥 < 𝑦 ↔ 𝑥 < 𝑧)) |
70 | 69 | biimpac 481 |
. . . . . . 7
⊢ ((𝑥 < 𝑦 ∧ 𝑦 = 𝑧) → 𝑥 < 𝑧) |
71 | 70, 64 | syl5 34 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 < 𝑦 ∧ 𝑦 = 𝑧) → 𝑥 ≤ 𝑧)) |
72 | 54, 34 | syldan 593 |
. . . . . . 7
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → 𝑥 ≤ 𝑥) |
73 | | eqtr 2841 |
. . . . . . . 8
⊢ ((𝑥 = 𝑦 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑧) |
74 | 73 | breq2d 5077 |
. . . . . . 7
⊢ ((𝑥 = 𝑦 ∧ 𝑦 = 𝑧) → (𝑥 ≤ 𝑥 ↔ 𝑥 ≤ 𝑧)) |
75 | 72, 74 | syl5ibcom 247 |
. . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 = 𝑦 ∧ 𝑦 = 𝑧) → 𝑥 ≤ 𝑧)) |
76 | 65, 68, 71, 75 | ccased 1033 |
. . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (((𝑥 < 𝑦 ∨ 𝑥 = 𝑦) ∧ (𝑦 < 𝑧 ∨ 𝑦 = 𝑧)) → 𝑥 ≤ 𝑧)) |
77 | 56, 59, 76 | syl2and 609 |
. . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) |
78 | 24, 25, 26, 34, 53, 77 | isposd 17564 |
. . 3
⊢ ((𝐾 ∈ 𝑉 ∧ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ )) → 𝐾 ∈ Poset) |
79 | 78 | ex 415 |
. 2
⊢ (𝐾 ∈ 𝑉 → (( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ ) → 𝐾 ∈ Poset)) |
80 | 22, 79 | impbid2 228 |
1
⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ Poset ↔ ( < Po 𝐵 ∧ ( I ↾ 𝐵) ⊆ ≤ ))) |