Proof of Theorem isprsd
Step | Hyp | Ref
| Expression |
1 | | isprsd.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈ 𝑉) |
2 | 1 | elexd 3452 |
. . 3
⊢ (𝜑 → 𝐾 ∈ V) |
3 | | eqid 2738 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
4 | | eqid 2738 |
. . . . 5
⊢
(le‘𝐾) =
(le‘𝐾) |
5 | 3, 4 | isprs 18015 |
. . . 4
⊢ (𝐾 ∈ Proset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
6 | 5 | baib 536 |
. . 3
⊢ (𝐾 ∈ V → (𝐾 ∈ Proset ↔
∀𝑥 ∈
(Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
7 | 2, 6 | syl 17 |
. 2
⊢ (𝜑 → (𝐾 ∈ Proset ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
8 | | isprsd.b |
. . 3
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
9 | | isprsd.l |
. . . . . . 7
⊢ (𝜑 → ≤ = (le‘𝐾)) |
10 | 9 | breqd 5085 |
. . . . . 6
⊢ (𝜑 → (𝑥 ≤ 𝑥 ↔ 𝑥(le‘𝐾)𝑥)) |
11 | 9 | breqd 5085 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ≤ 𝑦 ↔ 𝑥(le‘𝐾)𝑦)) |
12 | 9 | breqd 5085 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ≤ 𝑧 ↔ 𝑦(le‘𝐾)𝑧)) |
13 | 11, 12 | anbi12d 631 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) ↔ (𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧))) |
14 | 9 | breqd 5085 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ≤ 𝑧 ↔ 𝑥(le‘𝐾)𝑧)) |
15 | 13, 14 | imbi12d 345 |
. . . . . 6
⊢ (𝜑 → (((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧) ↔ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
16 | 10, 15 | anbi12d 631 |
. . . . 5
⊢ (𝜑 → ((𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
17 | 8, 16 | raleqbidv 3336 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
18 | 8, 17 | raleqbidv 3336 |
. . 3
⊢ (𝜑 → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
19 | 8, 18 | raleqbidv 3336 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)) ↔ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)∀𝑧 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
20 | 7, 19 | bitr4d 281 |
1
⊢ (𝜑 → (𝐾 ∈ Proset ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥 ≤ 𝑥 ∧ ((𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧) → 𝑥 ≤ 𝑧)))) |