Step | Hyp | Ref
| Expression |
1 | | ovexd 6720 |
. . 3
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ V) |
2 | | simp-4l 823 |
. . . . . . . 8
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝐾 ∈ Preset ) |
3 | | simp-4r 824 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝐴 ⊆ 𝐵) |
4 | | simpllr 815 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
5 | 3, 4 | sseldd 3637 |
. . . . . . . 8
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
6 | 2, 5 | jca 553 |
. . . . . . 7
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝐾 ∈ Preset ∧ 𝑥 ∈ 𝐵)) |
7 | | simplr 807 |
. . . . . . . 8
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
8 | 3, 7 | sseldd 3637 |
. . . . . . 7
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝐵) |
9 | | simpr 476 |
. . . . . . . 8
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
10 | 3, 9 | sseldd 3637 |
. . . . . . 7
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵) |
11 | | ressprs.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝐾) |
12 | | eqid 2651 |
. . . . . . . . . . . 12
⊢
(le‘𝐾) =
(le‘𝐾) |
13 | 11, 12 | isprs 16977 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ Preset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
14 | 13 | simprbi 479 |
. . . . . . . . . 10
⊢ (𝐾 ∈ Preset →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
15 | 14 | r19.21bi 2961 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Preset ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
16 | 15 | r19.21bi 2961 |
. . . . . . . 8
⊢ (((𝐾 ∈ Preset ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
17 | 16 | r19.21bi 2961 |
. . . . . . 7
⊢ ((((𝐾 ∈ Preset ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
18 | 6, 8, 10, 17 | syl21anc 1365 |
. . . . . 6
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
19 | 18 | ralrimiva 2995 |
. . . . 5
⊢ ((((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
20 | 19 | ralrimiva 2995 |
. . . 4
⊢ (((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
21 | 20 | ralrimiva 2995 |
. . 3
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
22 | | eqid 2651 |
. . . . . . 7
⊢ (𝐾 ↾s 𝐴) = (𝐾 ↾s 𝐴) |
23 | 22, 11 | ressbas2 15978 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘(𝐾 ↾s 𝐴))) |
24 | 23 | adantl 481 |
. . . . 5
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → 𝐴 = (Base‘(𝐾 ↾s 𝐴))) |
25 | | fvex 6239 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐾)
∈ V |
26 | 11, 25 | eqeltri 2726 |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
27 | 26 | ssex 4835 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
28 | 22, 12 | ressle 16106 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) |
29 | 27, 28 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝐵 → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) |
30 | 29 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) |
31 | 30 | breqd 4696 |
. . . . . . . 8
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝑥(le‘𝐾)𝑥 ↔ 𝑥(le‘(𝐾 ↾s 𝐴))𝑥)) |
32 | 30 | breqd 4696 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝑥(le‘𝐾)𝑦 ↔ 𝑥(le‘(𝐾 ↾s 𝐴))𝑦)) |
33 | 30 | breqd 4696 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝑦(le‘𝐾)𝑧 ↔ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧)) |
34 | 32, 33 | anbi12d 747 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) ↔ (𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧))) |
35 | 30 | breqd 4696 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝑥(le‘𝐾)𝑧 ↔ 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)) |
36 | 34, 35 | imbi12d 333 |
. . . . . . . 8
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧) ↔ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧))) |
37 | 31, 36 | anbi12d 747 |
. . . . . . 7
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → ((𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)) ↔ (𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
38 | 24, 37 | raleqbidv 3182 |
. . . . . 6
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)) ↔ ∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
39 | 24, 38 | raleqbidv 3182 |
. . . . 5
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)) ↔ ∀𝑦 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
40 | 24, 39 | raleqbidv 3182 |
. . . 4
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)) ↔ ∀𝑥 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
41 | 40 | anbi2d 740 |
. . 3
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (((𝐾 ↾s 𝐴) ∈ V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) ↔ ((𝐾 ↾s 𝐴) ∈ V ∧ ∀𝑥 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧))))) |
42 | 1, 21, 41 | mpbi2and 976 |
. 2
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → ((𝐾 ↾s 𝐴) ∈ V ∧ ∀𝑥 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
43 | | eqid 2651 |
. . 3
⊢
(Base‘(𝐾
↾s 𝐴)) =
(Base‘(𝐾
↾s 𝐴)) |
44 | | eqid 2651 |
. . 3
⊢
(le‘(𝐾
↾s 𝐴)) =
(le‘(𝐾
↾s 𝐴)) |
45 | 43, 44 | isprs 16977 |
. 2
⊢ ((𝐾 ↾s 𝐴) ∈ Preset ↔ ((𝐾 ↾s 𝐴) ∈ V ∧ ∀𝑥 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
46 | 42, 45 | sylibr 224 |
1
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Preset ) |