Proof of Theorem isposd
Step | Hyp | Ref
| Expression |
1 | | isposd.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈ 𝑉) |
2 | 1 | elexd 3418 |
. . 3
⊢ (𝜑 → 𝐾 ∈ V) |
3 | | isposd.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ≤ 𝑥) |
4 | 3 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ≤ 𝑥) |
5 | 4 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → 𝑥 ≤ 𝑥) |
6 | | isposd.2 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) |
7 | 6 | 3expb 1121 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) |
8 | 7 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦)) |
9 | | isposd.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) |
10 | 9 | 3exp2 1355 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))))) |
11 | 10 | imp42 430 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) |
12 | 5, 8, 11 | 3jca 1129 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑧 ∈ 𝐵) → (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))) |
13 | 12 | ralrimiva 3096 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))) |
14 | 13 | ralrimivva 3103 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))) |
15 | | isposd.b |
. . . . 5
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
16 | | isposd.l |
. . . . . . . . 9
⊢ (𝜑 → ≤ = (le‘𝐾)) |
17 | 16 | breqd 5041 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ≤ 𝑥 ↔ 𝑥(le‘𝐾)𝑥)) |
18 | 16 | breqd 5041 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ≤ 𝑦 ↔ 𝑥(le‘𝐾)𝑦)) |
19 | 16 | breqd 5041 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ≤ 𝑥 ↔ 𝑦(le‘𝐾)𝑥)) |
20 | 18, 19 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) ↔ (𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥))) |
21 | 20 | imbi1d 345 |
. . . . . . . 8
⊢ (𝜑 → (((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ↔ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦))) |
22 | 16 | breqd 5041 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ≤ 𝑧 ↔ 𝑦(le‘𝐾)𝑧)) |
23 | 18, 22 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) ↔ (𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧))) |
24 | 16 | breqd 5041 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ≤ 𝑧 ↔ 𝑥(le‘𝐾)𝑧)) |
25 | 23, 24 | imbi12d 348 |
. . . . . . . 8
⊢ (𝜑 → (((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧) ↔ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
26 | 17, 21, 25 | 3anbi123d 1437 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
27 | 15, 26 | raleqbidv 3304 |
. . . . . 6
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
28 | 15, 27 | raleqbidv 3304 |
. . . . 5
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
29 | 15, 28 | raleqbidv 3304 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
30 | 29 | anbi2d 632 |
. . 3
⊢ (𝜑 → ((𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥) → 𝑥 = 𝑦) ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧))) ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))))) |
31 | 2, 14, 30 | mpbi2and 712 |
. 2
⊢ (𝜑 → (𝐾 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
32 | | eqid 2738 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
33 | | eqid 2738 |
. . 3
⊢
(le‘𝐾) =
(le‘𝐾) |
34 | 32, 33 | ispos 17673 |
. 2
⊢ (𝐾 ∈ Poset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
35 | 31, 34 | sylibr 237 |
1
⊢ (𝜑 → 𝐾 ∈ Poset) |