Metamath Proof Explorer

Theorem resstos

Description: The restriction of a Toset is a Toset. (Contributed by Thierry Arnoux, 20-Jan-2018)

Ref Expression
Assertion resstos ⊢ F ∈ Toset ∧ A ∈ V → F ↾ 𝑠 A ∈ Toset

Proof

Step Hyp Ref Expression
1 tospos ⊢ F ∈ Toset → F ∈ Poset
2 resspos ⊢ F ∈ Poset ∧ A ∈ V → F ↾ 𝑠 A ∈ Poset
3 1 2 sylan ⊢ F ∈ Toset ∧ A ∈ V → F ↾ 𝑠 A ∈ Poset
4 eqid ⊢ F ↾ 𝑠 A = F ↾ 𝑠 A
5 eqid ⊢ Base F = Base F
6 4 5 ressbas ⊢ A ∈ V → A ∩ Base F = Base F ↾ 𝑠 A
7 inss2 ⊢ A ∩ Base F ⊆ Base F
8 6 7 eqsstrrdi ⊢ A ∈ V → Base F ↾ 𝑠 A ⊆ Base F
9 8 adantl ⊢ F ∈ Toset ∧ A ∈ V → Base F ↾ 𝑠 A ⊆ Base F
10 eqid ⊢ ≤ F = ≤ F
11 5 10 istos ⊢ F ∈ Toset ↔ F ∈ Poset ∧ ∀ x ∈ Base F ∀ y ∈ Base F x ≤ F y ∨ y ≤ F x
12 11 simprbi ⊢ F ∈ Toset → ∀ x ∈ Base F ∀ y ∈ Base F x ≤ F y ∨ y ≤ F x
13 12 adantr ⊢ F ∈ Toset ∧ A ∈ V → ∀ x ∈ Base F ∀ y ∈ Base F x ≤ F y ∨ y ≤ F x
14 ssralv ⊢ Base F ↾ 𝑠 A ⊆ Base F → ∀ x ∈ Base F ∀ y ∈ Base F x ≤ F y ∨ y ≤ F x → ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F x ≤ F y ∨ y ≤ F x
15 ssralv ⊢ Base F ↾ 𝑠 A ⊆ Base F → ∀ y ∈ Base F x ≤ F y ∨ y ≤ F x → ∀ y ∈ Base F ↾ 𝑠 A x ≤ F y ∨ y ≤ F x
16 15 ralimdv ⊢ Base F ↾ 𝑠 A ⊆ Base F → ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F x ≤ F y ∨ y ≤ F x → ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F ↾ 𝑠 A x ≤ F y ∨ y ≤ F x
17 14 16 syld ⊢ Base F ↾ 𝑠 A ⊆ Base F → ∀ x ∈ Base F ∀ y ∈ Base F x ≤ F y ∨ y ≤ F x → ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F ↾ 𝑠 A x ≤ F y ∨ y ≤ F x
18 9 13 17 sylc ⊢ F ∈ Toset ∧ A ∈ V → ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F ↾ 𝑠 A x ≤ F y ∨ y ≤ F x
19 4 10 ressle ⊢ A ∈ V → ≤ F = ≤ F ↾ 𝑠 A
20 19 breqd ⊢ A ∈ V → x ≤ F y ↔ x ≤ F ↾ 𝑠 A y
21 19 breqd ⊢ A ∈ V → y ≤ F x ↔ y ≤ F ↾ 𝑠 A x
22 20 21 orbi12d ⊢ A ∈ V → x ≤ F y ∨ y ≤ F x ↔ x ≤ F ↾ 𝑠 A y ∨ y ≤ F ↾ 𝑠 A x
23 22 2ralbidv ⊢ A ∈ V → ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F ↾ 𝑠 A x ≤ F y ∨ y ≤ F x ↔ ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F ↾ 𝑠 A x ≤ F ↾ 𝑠 A y ∨ y ≤ F ↾ 𝑠 A x
24 23 adantl ⊢ F ∈ Toset ∧ A ∈ V → ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F ↾ 𝑠 A x ≤ F y ∨ y ≤ F x ↔ ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F ↾ 𝑠 A x ≤ F ↾ 𝑠 A y ∨ y ≤ F ↾ 𝑠 A x
25 18 24 mpbid ⊢ F ∈ Toset ∧ A ∈ V → ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F ↾ 𝑠 A x ≤ F ↾ 𝑠 A y ∨ y ≤ F ↾ 𝑠 A x
26 eqid ⊢ Base F ↾ 𝑠 A = Base F ↾ 𝑠 A
27 eqid ⊢ ≤ F ↾ 𝑠 A = ≤ F ↾ 𝑠 A
28 26 27 istos ⊢ F ↾ 𝑠 A ∈ Toset ↔ F ↾ 𝑠 A ∈ Poset ∧ ∀ x ∈ Base F ↾ 𝑠 A ∀ y ∈ Base F ↾ 𝑠 A x ≤ F ↾ 𝑠 A y ∨ y ≤ F ↾ 𝑠 A x
29 3 25 28 sylanbrc ⊢ F ∈ Toset ∧ A ∈ V → F ↾ 𝑠 A ∈ Toset