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