Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑝 = 𝐾 → (Base‘𝑝) = (Base‘𝐾)) |
2 | | ispos.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝐾) |
3 | 1, 2 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑝 = 𝐾 → (Base‘𝑝) = 𝐵) |
4 | 3 | eqeq2d 2620 |
. . . . 5
⊢ (𝑝 = 𝐾 → (𝑏 = (Base‘𝑝) ↔ 𝑏 = 𝐵)) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑝 = 𝐾 → (le‘𝑝) = (le‘𝐾)) |
6 | | ispos.l |
. . . . . . 7
⊢ ≤ =
(le‘𝐾) |
7 | 5, 6 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑝 = 𝐾 → (le‘𝑝) = ≤ ) |
8 | 7 | eqeq2d 2620 |
. . . . 5
⊢ (𝑝 = 𝐾 → (𝑟 = (le‘𝑝) ↔ 𝑟 = ≤ )) |
9 | 4, 8 | 3anbi12d 1392 |
. . . 4
⊢ (𝑝 = 𝐾 → ((𝑏 = (Base‘𝑝) ∧ 𝑟 = (le‘𝑝) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))) ↔ (𝑏 = 𝐵 ∧ 𝑟 = ≤ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))))) |
10 | 9 | 2exbidv 1839 |
. . 3
⊢ (𝑝 = 𝐾 → (∃𝑏∃𝑟(𝑏 = (Base‘𝑝) ∧ 𝑟 = (le‘𝑝) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))) ↔ ∃𝑏∃𝑟(𝑏 = 𝐵 ∧ 𝑟 = ≤ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))))) |
11 | | df-poset 16769 |
. . 3
⊢ Poset =
{𝑝 ∣ ∃𝑏∃𝑟(𝑏 = (Base‘𝑝) ∧ 𝑟 = (le‘𝑝) ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))} |
12 | 10, 11 | elab4g 3324 |
. 2
⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∃𝑏∃𝑟(𝑏 = 𝐵 ∧ 𝑟 = ≤ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))))) |
13 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝐾)
∈ V |
14 | 2, 13 | eqeltri 2684 |
. . . 4
⊢ 𝐵 ∈ V |
15 | | fvex 6113 |
. . . . 5
⊢
(le‘𝐾) ∈
V |
16 | 6, 15 | eqeltri 2684 |
. . . 4
⊢ ≤ ∈
V |
17 | | raleq 3115 |
. . . . . 6
⊢ (𝑏 = 𝐵 → (∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))) |
18 | 17 | raleqbi1dv 3123 |
. . . . 5
⊢ (𝑏 = 𝐵 → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)) ↔ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))) |
19 | 18 | raleqbi1dv 3123 |
. . . 4
⊢ (𝑏 = 𝐵 → (∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))) |
20 | | breq 4585 |
. . . . . . 7
⊢ (𝑟 = ≤ → (𝑥𝑟𝑥 ↔ 𝑥 ≤ 𝑥)) |
21 | | breq 4585 |
. . . . . . . . 9
⊢ (𝑟 = ≤ → (𝑥𝑟𝑦 ↔ 𝑥 ≤ 𝑦)) |
22 | | breq 4585 |
. . . . . . . . 9
⊢ (𝑟 = ≤ → (𝑦𝑟𝑥 ↔ 𝑦 ≤ 𝑥)) |
23 | 21, 22 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑟 = ≤ → ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥))) |
24 | 23 | imbi1d 330 |
. . . . . . 7
⊢ (𝑟 = ≤ → (((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ↔ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦))) |
25 | | breq 4585 |
. . . . . . . . 9
⊢ (𝑟 = ≤ → (𝑦𝑟𝑧 ↔ 𝑦 ≤ 𝑧)) |
26 | 21, 25 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑟 = ≤ → ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) ↔ (𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧))) |
27 | | breq 4585 |
. . . . . . . 8
⊢ (𝑟 = ≤ → (𝑥𝑟𝑧 ↔ 𝑥 ≤ 𝑧)) |
28 | 26, 27 | imbi12d 333 |
. . . . . . 7
⊢ (𝑟 = ≤ → (((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧) ↔ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))) |
29 | 20, 24, 28 | 3anbi123d 1391 |
. . . . . 6
⊢ (𝑟 = ≤ → ((𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)) ↔ (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) |
30 | 29 | ralbidv 2969 |
. . . . 5
⊢ (𝑟 = ≤ → (∀𝑧 ∈ 𝐵 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)) ↔ ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) |
31 | 30 | 2ralbidv 2972 |
. . . 4
⊢ (𝑟 = ≤ → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) |
32 | 14, 16, 19, 31 | ceqsex2v 3218 |
. . 3
⊢
(∃𝑏∃𝑟(𝑏 = 𝐵 ∧ 𝑟 = ≤ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧))) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))) |
33 | 32 | anbi2i 726 |
. 2
⊢ ((𝐾 ∈ V ∧ ∃𝑏∃𝑟(𝑏 = 𝐵 ∧ 𝑟 = ≤ ∧ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 (𝑥𝑟𝑥 ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑥) → 𝑥 = 𝑦) ∧ ((𝑥𝑟𝑦 ∧ 𝑦𝑟𝑧) → 𝑥𝑟𝑧)))) ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) |
34 | 12, 33 | bitri 263 |
1
⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) |