Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . 4
⊢ (𝐾 ↾s 𝐴) ∈ V |
2 | 1 | a1i 11 |
. . 3
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ V) |
3 | | simp-4l 802 |
. . . . . . . 8
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝐾 ∈ Preset ) |
4 | | simp-4r 803 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝐴 ⊆ 𝐵) |
5 | | simpllr 795 |
. . . . . . . . 9
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
6 | 4, 5 | sseldd 3569 |
. . . . . . . 8
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑥 ∈ 𝐵) |
7 | 3, 6 | jca 553 |
. . . . . . 7
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝐾 ∈ Preset ∧ 𝑥 ∈ 𝐵)) |
8 | | simplr 788 |
. . . . . . . 8
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
9 | 4, 8 | sseldd 3569 |
. . . . . . 7
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑦 ∈ 𝐵) |
10 | | simpr 476 |
. . . . . . . 8
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
11 | 4, 10 | sseldd 3569 |
. . . . . . 7
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐵) |
12 | | ressprs.b |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝐾) |
13 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(le‘𝐾) =
(le‘𝐾) |
14 | 12, 13 | isprs 16753 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ Preset ↔ (𝐾 ∈ V ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)))) |
15 | 14 | simprbi 479 |
. . . . . . . . . 10
⊢ (𝐾 ∈ Preset →
∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
16 | 15 | r19.21bi 2916 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Preset ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
17 | 16 | r19.21bi 2916 |
. . . . . . . 8
⊢ (((𝐾 ∈ Preset ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) → ∀𝑧 ∈ 𝐵 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
18 | 17 | r19.21bi 2916 |
. . . . . . 7
⊢ ((((𝐾 ∈ Preset ∧ 𝑥 ∈ 𝐵) ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 ∈ 𝐵) → (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
19 | 7, 9, 11, 18 | syl21anc 1317 |
. . . . . 6
⊢
(((((𝐾 ∈ Preset
∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
20 | 19 | ralrimiva 2949 |
. . . . 5
⊢ ((((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐴) → ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
21 | 20 | ralrimiva 2949 |
. . . 4
⊢ (((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) ∧ 𝑥 ∈ 𝐴) → ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
22 | 21 | ralrimiva 2949 |
. . 3
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) |
23 | | eqid 2610 |
. . . . . . 7
⊢ (𝐾 ↾s 𝐴) = (𝐾 ↾s 𝐴) |
24 | 23, 12 | ressbas2 15758 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 → 𝐴 = (Base‘(𝐾 ↾s 𝐴))) |
25 | 24 | adantl 481 |
. . . . 5
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → 𝐴 = (Base‘(𝐾 ↾s 𝐴))) |
26 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐾)
∈ V |
27 | 12, 26 | eqeltri 2684 |
. . . . . . . . . . . 12
⊢ 𝐵 ∈ V |
28 | 27 | ssex 4730 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
29 | 23, 13 | ressle 15882 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ V → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝐴 ⊆ 𝐵 → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) |
31 | 30 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (le‘𝐾) = (le‘(𝐾 ↾s 𝐴))) |
32 | 31 | breqd 4594 |
. . . . . . . 8
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝑥(le‘𝐾)𝑥 ↔ 𝑥(le‘(𝐾 ↾s 𝐴))𝑥)) |
33 | 31 | breqd 4594 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝑥(le‘𝐾)𝑦 ↔ 𝑥(le‘(𝐾 ↾s 𝐴))𝑦)) |
34 | 31 | breqd 4594 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝑦(le‘𝐾)𝑧 ↔ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧)) |
35 | 33, 34 | anbi12d 743 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) ↔ (𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧))) |
36 | 31 | breqd 4594 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝑥(le‘𝐾)𝑧 ↔ 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)) |
37 | 35, 36 | imbi12d 333 |
. . . . . . . 8
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧) ↔ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧))) |
38 | 32, 37 | anbi12d 743 |
. . . . . . 7
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → ((𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)) ↔ (𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
39 | 25, 38 | raleqbidv 3129 |
. . . . . 6
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)) ↔ ∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
40 | 25, 39 | raleqbidv 3129 |
. . . . 5
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)) ↔ ∀𝑦 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
41 | 25, 40 | raleqbidv 3129 |
. . . 4
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧)) ↔ ∀𝑥 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
42 | 41 | anbi2d 736 |
. . 3
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (((𝐾 ↾s 𝐴) ∈ V ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥(le‘𝐾)𝑥 ∧ ((𝑥(le‘𝐾)𝑦 ∧ 𝑦(le‘𝐾)𝑧) → 𝑥(le‘𝐾)𝑧))) ↔ ((𝐾 ↾s 𝐴) ∈ V ∧ ∀𝑥 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧))))) |
43 | 2, 22, 42 | mpbi2and 958 |
. 2
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → ((𝐾 ↾s 𝐴) ∈ V ∧ ∀𝑥 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
44 | | eqid 2610 |
. . 3
⊢
(Base‘(𝐾
↾s 𝐴)) =
(Base‘(𝐾
↾s 𝐴)) |
45 | | eqid 2610 |
. . 3
⊢
(le‘(𝐾
↾s 𝐴)) =
(le‘(𝐾
↾s 𝐴)) |
46 | 44, 45 | isprs 16753 |
. 2
⊢ ((𝐾 ↾s 𝐴) ∈ Preset ↔ ((𝐾 ↾s 𝐴) ∈ V ∧ ∀𝑥 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐾 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐾 ↾s 𝐴))(𝑥(le‘(𝐾 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐾 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐾 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐾 ↾s 𝐴))𝑧)))) |
47 | 43, 46 | sylibr 223 |
1
⊢ ((𝐾 ∈ Preset ∧ 𝐴 ⊆ 𝐵) → (𝐾 ↾s 𝐴) ∈ Preset ) |