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 ⊢BaseF=BaseF
6 4 5 ressbas ⊢A∈V→A∩BaseF=BaseF↾𝑠A
7 inss2 ⊢A∩BaseF⊆BaseF
8 6 7 eqsstrrdi ⊢A∈V→BaseF↾𝑠A⊆BaseF
9 8 adantl ⊢F∈Toset∧A∈V→BaseF↾𝑠A⊆BaseF
10 eqid ⊢≤F=≤F
11 5 10 istos ⊢F∈Toset↔F∈Poset∧∀x∈BaseF∀y∈BaseFx≤Fy∨y≤Fx
12 11 simprbi ⊢F∈Toset→∀x∈BaseF∀y∈BaseFx≤Fy∨y≤Fx
13 12 adantr ⊢F∈Toset∧A∈V→∀x∈BaseF∀y∈BaseFx≤Fy∨y≤Fx
14 ssralv ⊢BaseF↾𝑠A⊆BaseF→∀x∈BaseF∀y∈BaseFx≤Fy∨y≤Fx→∀x∈BaseF↾𝑠A∀y∈BaseFx≤Fy∨y≤Fx
15 ssralv ⊢BaseF↾𝑠A⊆BaseF→∀y∈BaseFx≤Fy∨y≤Fx→∀y∈BaseF↾𝑠Ax≤Fy∨y≤Fx
16 15 ralimdv ⊢BaseF↾𝑠A⊆BaseF→∀x∈BaseF↾𝑠A∀y∈BaseFx≤Fy∨y≤Fx→∀x∈BaseF↾𝑠A∀y∈BaseF↾𝑠Ax≤Fy∨y≤Fx
17 14 16 syld ⊢BaseF↾𝑠A⊆BaseF→∀x∈BaseF∀y∈BaseFx≤Fy∨y≤Fx→∀x∈BaseF↾𝑠A∀y∈BaseF↾𝑠Ax≤Fy∨y≤Fx
18 9 13 17 sylc ⊢F∈Toset∧A∈V→∀x∈BaseF↾𝑠A∀y∈BaseF↾𝑠Ax≤Fy∨y≤Fx
19 4 10 ressle ⊢A∈V→≤F=≤F↾𝑠A
20 19 breqd ⊢A∈V→x≤Fy↔x≤F↾𝑠Ay
21 19 breqd ⊢A∈V→y≤Fx↔y≤F↾𝑠Ax
22 20 21 orbi12d ⊢A∈V→x≤Fy∨y≤Fx↔x≤F↾𝑠Ay∨y≤F↾𝑠Ax
23 22 2ralbidv ⊢A∈V→∀x∈BaseF↾𝑠A∀y∈BaseF↾𝑠Ax≤Fy∨y≤Fx↔∀x∈BaseF↾𝑠A∀y∈BaseF↾𝑠Ax≤F↾𝑠Ay∨y≤F↾𝑠Ax
24 23 adantl ⊢F∈Toset∧A∈V→∀x∈BaseF↾𝑠A∀y∈BaseF↾𝑠Ax≤Fy∨y≤Fx↔∀x∈BaseF↾𝑠A∀y∈BaseF↾𝑠Ax≤F↾𝑠Ay∨y≤F↾𝑠Ax
25 18 24 mpbid ⊢F∈Toset∧A∈V→∀x∈BaseF↾𝑠A∀y∈BaseF↾𝑠Ax≤F↾𝑠Ay∨y≤F↾𝑠Ax
26 eqid ⊢BaseF↾𝑠A=BaseF↾𝑠A
27 eqid ⊢≤F↾𝑠A=≤F↾𝑠A
28 26 27 istos ⊢F↾𝑠A∈Toset↔F↾𝑠A∈Poset∧∀x∈BaseF↾𝑠A∀y∈BaseF↾𝑠Ax≤F↾𝑠Ay∨y≤F↾𝑠Ax
29 3 25 28 sylanbrc ⊢F∈Toset∧A∈V→F↾𝑠A∈Toset