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 e. Toset /\ A e. V ) -> ( F |`s A ) e. Toset )

Proof

Step Hyp Ref Expression
1 tospos 
 |-  ( F e. Toset -> F e. Poset )
2 resspos 
 |-  ( ( F e. Poset /\ A e. V ) -> ( F |`s A ) e. Poset )
3 1 2 sylan 
 |-  ( ( F e. Toset /\ A e. V ) -> ( F |`s A ) e. Poset )
4 eqid 
 |-  ( F |`s A ) = ( F |`s A )
5 eqid 
 |-  ( Base ` F ) = ( Base ` F )
6 4 5 ressbas 
 |-  ( A e. V -> ( A i^i ( Base ` F ) ) = ( Base ` ( F |`s A ) ) )
7 inss2 
 |-  ( A i^i ( Base ` F ) ) C_ ( Base ` F )
8 6 7 eqsstrrdi 
 |-  ( A e. V -> ( Base ` ( F |`s A ) ) C_ ( Base ` F ) )
9 8 adantl 
 |-  ( ( F e. Toset /\ A e. V ) -> ( Base ` ( F |`s A ) ) C_ ( Base ` F ) )
10 eqid 
 |-  ( le ` F ) = ( le ` F )
11 5 10 istos 
 |-  ( F e. Toset <-> ( F e. Poset /\ A. x e. ( Base ` F ) A. y e. ( Base ` F ) ( x ( le ` F ) y \/ y ( le ` F ) x ) ) )
12 11 simprbi 
 |-  ( F e. Toset -> A. x e. ( Base ` F ) A. y e. ( Base ` F ) ( x ( le ` F ) y \/ y ( le ` F ) x ) )
13 12 adantr 
 |-  ( ( F e. Toset /\ A e. V ) -> A. x e. ( Base ` F ) A. y e. ( Base ` F ) ( x ( le ` F ) y \/ y ( le ` F ) x ) )
14 ssralv 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. x e. ( Base ` F ) A. y e. ( Base ` F ) ( x ( le ` F ) y \/ y ( le ` F ) x ) -> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` F ) ( x ( le ` F ) y \/ y ( le ` F ) x ) ) )
15 ssralv 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. y e. ( Base ` F ) ( x ( le ` F ) y \/ y ( le ` F ) x ) -> A. y e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) y \/ y ( le ` F ) x ) ) )
16 15 ralimdv 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` F ) ( x ( le ` F ) y \/ y ( le ` F ) x ) -> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) y \/ y ( le ` F ) x ) ) )
17 14 16 syld 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. x e. ( Base ` F ) A. y e. ( Base ` F ) ( x ( le ` F ) y \/ y ( le ` F ) x ) -> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) y \/ y ( le ` F ) x ) ) )
18 9 13 17 sylc 
 |-  ( ( F e. Toset /\ A e. V ) -> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) y \/ y ( le ` F ) x ) )
19 4 10 ressle 
 |-  ( A e. V -> ( le ` F ) = ( le ` ( F |`s A ) ) )
20 19 breqd 
 |-  ( A e. V -> ( x ( le ` F ) y <-> x ( le ` ( F |`s A ) ) y ) )
21 19 breqd 
 |-  ( A e. V -> ( y ( le ` F ) x <-> y ( le ` ( F |`s A ) ) x ) )
22 20 21 orbi12d 
 |-  ( A e. V -> ( ( x ( le ` F ) y \/ y ( le ` F ) x ) <-> ( x ( le ` ( F |`s A ) ) y \/ y ( le ` ( F |`s A ) ) x ) ) )
23 22 2ralbidv 
 |-  ( A e. V -> ( A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) y \/ y ( le ` F ) x ) <-> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) ( x ( le ` ( F |`s A ) ) y \/ y ( le ` ( F |`s A ) ) x ) ) )
24 23 adantl 
 |-  ( ( F e. Toset /\ A e. V ) -> ( A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) y \/ y ( le ` F ) x ) <-> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) ( x ( le ` ( F |`s A ) ) y \/ y ( le ` ( F |`s A ) ) x ) ) )
25 18 24 mpbid 
 |-  ( ( F e. Toset /\ A e. V ) -> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) ( x ( le ` ( F |`s A ) ) y \/ y ( le ` ( F |`s A ) ) x ) )
26 eqid 
 |-  ( Base ` ( F |`s A ) ) = ( Base ` ( F |`s A ) )
27 eqid 
 |-  ( le ` ( F |`s A ) ) = ( le ` ( F |`s A ) )
28 26 27 istos 
 |-  ( ( F |`s A ) e. Toset <-> ( ( F |`s A ) e. Poset /\ A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) ( x ( le ` ( F |`s A ) ) y \/ y ( le ` ( F |`s A ) ) x ) ) )
29 3 25 28 sylanbrc 
 |-  ( ( F e. Toset /\ A e. V ) -> ( F |`s A ) e. Toset )