Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . 3
⊢ (𝐹 ↾s 𝐴) ∈ V |
2 | 1 | a1i 11 |
. 2
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ V) |
3 | | eqid 2610 |
. . . . . . 7
⊢ (𝐹 ↾s 𝐴) = (𝐹 ↾s 𝐴) |
4 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝐹) =
(Base‘𝐹) |
5 | 3, 4 | ressbas 15757 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ (Base‘𝐹)) = (Base‘(𝐹 ↾s 𝐴))) |
6 | | inss2 3796 |
. . . . . 6
⊢ (𝐴 ∩ (Base‘𝐹)) ⊆ (Base‘𝐹) |
7 | 5, 6 | syl6eqssr 3619 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (Base‘(𝐹 ↾s 𝐴)) ⊆ (Base‘𝐹)) |
8 | 7 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → (Base‘(𝐹 ↾s 𝐴)) ⊆ (Base‘𝐹)) |
9 | | eqid 2610 |
. . . . . . 7
⊢
(le‘𝐹) =
(le‘𝐹) |
10 | 4, 9 | ispos 16770 |
. . . . . 6
⊢ (𝐹 ∈ Poset ↔ (𝐹 ∈ V ∧ ∀𝑥 ∈ (Base‘𝐹)∀𝑦 ∈ (Base‘𝐹)∀𝑧 ∈ (Base‘𝐹)(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)))) |
11 | 10 | simprbi 479 |
. . . . 5
⊢ (𝐹 ∈ Poset →
∀𝑥 ∈
(Base‘𝐹)∀𝑦 ∈ (Base‘𝐹)∀𝑧 ∈ (Base‘𝐹)(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧))) |
12 | 11 | adantr 480 |
. . . 4
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → ∀𝑥 ∈ (Base‘𝐹)∀𝑦 ∈ (Base‘𝐹)∀𝑧 ∈ (Base‘𝐹)(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧))) |
13 | | ssralv 3629 |
. . . . . . . 8
⊢
((Base‘(𝐹
↾s 𝐴))
⊆ (Base‘𝐹)
→ (∀𝑧 ∈
(Base‘𝐹)(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) → ∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)))) |
14 | 13 | ralimdv 2946 |
. . . . . . 7
⊢
((Base‘(𝐹
↾s 𝐴))
⊆ (Base‘𝐹)
→ (∀𝑦 ∈
(Base‘𝐹)∀𝑧 ∈ (Base‘𝐹)(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) → ∀𝑦 ∈ (Base‘𝐹)∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)))) |
15 | | ssralv 3629 |
. . . . . . 7
⊢
((Base‘(𝐹
↾s 𝐴))
⊆ (Base‘𝐹)
→ (∀𝑦 ∈
(Base‘𝐹)∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) → ∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)))) |
16 | 14, 15 | syld 46 |
. . . . . 6
⊢
((Base‘(𝐹
↾s 𝐴))
⊆ (Base‘𝐹)
→ (∀𝑦 ∈
(Base‘𝐹)∀𝑧 ∈ (Base‘𝐹)(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) → ∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)))) |
17 | 16 | ralimdv 2946 |
. . . . 5
⊢
((Base‘(𝐹
↾s 𝐴))
⊆ (Base‘𝐹)
→ (∀𝑥 ∈
(Base‘𝐹)∀𝑦 ∈ (Base‘𝐹)∀𝑧 ∈ (Base‘𝐹)(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) → ∀𝑥 ∈ (Base‘𝐹)∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)))) |
18 | | ssralv 3629 |
. . . . 5
⊢
((Base‘(𝐹
↾s 𝐴))
⊆ (Base‘𝐹)
→ (∀𝑥 ∈
(Base‘𝐹)∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) → ∀𝑥 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)))) |
19 | 17, 18 | syld 46 |
. . . 4
⊢
((Base‘(𝐹
↾s 𝐴))
⊆ (Base‘𝐹)
→ (∀𝑥 ∈
(Base‘𝐹)∀𝑦 ∈ (Base‘𝐹)∀𝑧 ∈ (Base‘𝐹)(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) → ∀𝑥 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)))) |
20 | 8, 12, 19 | sylc 63 |
. . 3
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → ∀𝑥 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧))) |
21 | 3, 9 | ressle 15882 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (le‘𝐹) = (le‘(𝐹 ↾s 𝐴))) |
22 | 21 | adantl 481 |
. . . 4
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → (le‘𝐹) = (le‘(𝐹 ↾s 𝐴))) |
23 | | breq 4585 |
. . . . . . 7
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ (𝑥(le‘𝐹)𝑥 ↔ 𝑥(le‘(𝐹 ↾s 𝐴))𝑥)) |
24 | | breq 4585 |
. . . . . . . . 9
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ (𝑥(le‘𝐹)𝑦 ↔ 𝑥(le‘(𝐹 ↾s 𝐴))𝑦)) |
25 | | breq 4585 |
. . . . . . . . 9
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ (𝑦(le‘𝐹)𝑥 ↔ 𝑦(le‘(𝐹 ↾s 𝐴))𝑥)) |
26 | 24, 25 | anbi12d 743 |
. . . . . . . 8
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) ↔ (𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑥))) |
27 | 26 | imbi1d 330 |
. . . . . . 7
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ (((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ↔ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑥) → 𝑥 = 𝑦))) |
28 | | breq 4585 |
. . . . . . . . 9
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ (𝑦(le‘𝐹)𝑧 ↔ 𝑦(le‘(𝐹 ↾s 𝐴))𝑧)) |
29 | 24, 28 | anbi12d 743 |
. . . . . . . 8
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) ↔ (𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑧))) |
30 | | breq 4585 |
. . . . . . . 8
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ (𝑥(le‘𝐹)𝑧 ↔ 𝑥(le‘(𝐹 ↾s 𝐴))𝑧)) |
31 | 29, 30 | imbi12d 333 |
. . . . . . 7
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ (((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧) ↔ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐹 ↾s 𝐴))𝑧))) |
32 | 23, 27, 31 | 3anbi123d 1391 |
. . . . . 6
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ ((𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) ↔ (𝑥(le‘(𝐹 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐹 ↾s 𝐴))𝑧)))) |
33 | 32 | ralbidv 2969 |
. . . . 5
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ (∀𝑧 ∈
(Base‘(𝐹
↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) ↔ ∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘(𝐹 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐹 ↾s 𝐴))𝑧)))) |
34 | 33 | 2ralbidv 2972 |
. . . 4
⊢
((le‘𝐹) =
(le‘(𝐹
↾s 𝐴))
→ (∀𝑥 ∈
(Base‘(𝐹
↾s 𝐴))∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) ↔ ∀𝑥 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘(𝐹 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐹 ↾s 𝐴))𝑧)))) |
35 | 22, 34 | syl 17 |
. . 3
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → (∀𝑥 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘𝐹)𝑥 ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘𝐹)𝑦 ∧ 𝑦(le‘𝐹)𝑧) → 𝑥(le‘𝐹)𝑧)) ↔ ∀𝑥 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘(𝐹 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐹 ↾s 𝐴))𝑧)))) |
36 | 20, 35 | mpbid 221 |
. 2
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → ∀𝑥 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘(𝐹 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐹 ↾s 𝐴))𝑧))) |
37 | | eqid 2610 |
. . 3
⊢
(Base‘(𝐹
↾s 𝐴)) =
(Base‘(𝐹
↾s 𝐴)) |
38 | | eqid 2610 |
. . 3
⊢
(le‘(𝐹
↾s 𝐴)) =
(le‘(𝐹
↾s 𝐴)) |
39 | 37, 38 | ispos 16770 |
. 2
⊢ ((𝐹 ↾s 𝐴) ∈ Poset ↔ ((𝐹 ↾s 𝐴) ∈ V ∧ ∀𝑥 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑦 ∈ (Base‘(𝐹 ↾s 𝐴))∀𝑧 ∈ (Base‘(𝐹 ↾s 𝐴))(𝑥(le‘(𝐹 ↾s 𝐴))𝑥 ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑥) → 𝑥 = 𝑦) ∧ ((𝑥(le‘(𝐹 ↾s 𝐴))𝑦 ∧ 𝑦(le‘(𝐹 ↾s 𝐴))𝑧) → 𝑥(le‘(𝐹 ↾s 𝐴))𝑧)))) |
40 | 2, 36, 39 | sylanbrc 695 |
1
⊢ ((𝐹 ∈ Poset ∧ 𝐴 ∈ 𝑉) → (𝐹 ↾s 𝐴) ∈ Poset) |