Metamath Proof Explorer

Theorem resspos

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

Ref Expression
Assertion resspos 
|- ( ( F e. Poset /\ A e. V ) -> ( F |`s A ) e. Poset )

Proof

Step Hyp Ref Expression
1 ovexd 
 |-  ( ( F e. Poset /\ A e. V ) -> ( F |`s A ) e. _V )
2 eqid 
 |-  ( F |`s A ) = ( F |`s A )
3 eqid 
 |-  ( Base ` F ) = ( Base ` F )
4 2 3 ressbas 
 |-  ( A e. V -> ( A i^i ( Base ` F ) ) = ( Base ` ( F |`s A ) ) )
5 inss2 
 |-  ( A i^i ( Base ` F ) ) C_ ( Base ` F )
6 4 5 eqsstrrdi 
 |-  ( A e. V -> ( Base ` ( F |`s A ) ) C_ ( Base ` F ) )
7 6 adantl 
 |-  ( ( F e. Poset /\ A e. V ) -> ( Base ` ( F |`s A ) ) C_ ( Base ` F ) )
8 eqid 
 |-  ( le ` F ) = ( le ` F )
9 3 8 ispos 
 |-  ( F e. Poset <-> ( F e. _V /\ A. x e. ( Base ` F ) A. y e. ( Base ` F ) A. z e. ( Base ` F ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) ) )
10 9 simprbi 
 |-  ( F e. Poset -> A. x e. ( Base ` F ) A. y e. ( Base ` F ) A. z e. ( Base ` F ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) )
11 10 adantr 
 |-  ( ( F e. Poset /\ A e. V ) -> A. x e. ( Base ` F ) A. y e. ( Base ` F ) A. z e. ( Base ` F ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) )
12 ssralv 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. z e. ( Base ` F ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) -> A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) ) )
13 12 ralimdv 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. y e. ( Base ` F ) A. z e. ( Base ` F ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) -> A. y e. ( Base ` F ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) ) )
14 ssralv 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. y e. ( Base ` F ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) -> A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) ) )
15 13 14 syld 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. y e. ( Base ` F ) A. z e. ( Base ` F ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) -> A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) ) )
16 15 ralimdv 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. x e. ( Base ` F ) A. y e. ( Base ` F ) A. z e. ( Base ` F ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) -> A. x e. ( Base ` F ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) ) )
17 ssralv 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. x e. ( Base ` F ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) -> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) ) )
18 16 17 syld 
 |-  ( ( Base ` ( F |`s A ) ) C_ ( Base ` F ) -> ( A. x e. ( Base ` F ) A. y e. ( Base ` F ) A. z e. ( Base ` F ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) -> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) ) )
19 7 11 18 sylc 
 |-  ( ( F e. Poset /\ A e. V ) -> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) )
20 2 8 ressle 
 |-  ( A e. V -> ( le ` F ) = ( le ` ( F |`s A ) ) )
21 20 adantl 
 |-  ( ( F e. Poset /\ A e. V ) -> ( le ` F ) = ( le ` ( F |`s A ) ) )
22 breq 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( x ( le ` F ) x <-> x ( le ` ( F |`s A ) ) x ) )
23 breq 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( x ( le ` F ) y <-> x ( le ` ( F |`s A ) ) y ) )
24 breq 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( y ( le ` F ) x <-> y ( le ` ( F |`s A ) ) x ) )
25 23 24 anbi12d 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( ( x ( le ` F ) y /\ y ( le ` F ) x ) <-> ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) x ) ) )
26 25 imbi1d 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) <-> ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) x ) -> x = y ) ) )
27 breq 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( y ( le ` F ) z <-> y ( le ` ( F |`s A ) ) z ) )
28 23 27 anbi12d 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( ( x ( le ` F ) y /\ y ( le ` F ) z ) <-> ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) z ) ) )
29 breq 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( x ( le ` F ) z <-> x ( le ` ( F |`s A ) ) z ) )
30 28 29 imbi12d 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) <-> ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) z ) -> x ( le ` ( F |`s A ) ) z ) ) )
31 22 26 30 3anbi123d 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) <-> ( x ( le ` ( F |`s A ) ) x /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) x ) -> x = y ) /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) z ) -> x ( le ` ( F |`s A ) ) z ) ) ) )
32 31 ralbidv 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) <-> A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` ( F |`s A ) ) x /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) x ) -> x = y ) /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) z ) -> x ( le ` ( F |`s A ) ) z ) ) ) )
33 32 2ralbidv 
 |-  ( ( le ` F ) = ( le ` ( F |`s A ) ) -> ( A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) <-> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` ( F |`s A ) ) x /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) x ) -> x = y ) /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) z ) -> x ( le ` ( F |`s A ) ) z ) ) ) )
34 21 33 syl 
 |-  ( ( F e. Poset /\ A e. V ) -> ( A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` F ) x /\ ( ( x ( le ` F ) y /\ y ( le ` F ) x ) -> x = y ) /\ ( ( x ( le ` F ) y /\ y ( le ` F ) z ) -> x ( le ` F ) z ) ) <-> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` ( F |`s A ) ) x /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) x ) -> x = y ) /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) z ) -> x ( le ` ( F |`s A ) ) z ) ) ) )
35 19 34 mpbid 
 |-  ( ( F e. Poset /\ A e. V ) -> A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` ( F |`s A ) ) x /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) x ) -> x = y ) /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) z ) -> x ( le ` ( F |`s A ) ) z ) ) )
36 eqid 
 |-  ( Base ` ( F |`s A ) ) = ( Base ` ( F |`s A ) )
37 eqid 
 |-  ( le ` ( F |`s A ) ) = ( le ` ( F |`s A ) )
38 36 37 ispos 
 |-  ( ( F |`s A ) e. Poset <-> ( ( F |`s A ) e. _V /\ A. x e. ( Base ` ( F |`s A ) ) A. y e. ( Base ` ( F |`s A ) ) A. z e. ( Base ` ( F |`s A ) ) ( x ( le ` ( F |`s A ) ) x /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) x ) -> x = y ) /\ ( ( x ( le ` ( F |`s A ) ) y /\ y ( le ` ( F |`s A ) ) z ) -> x ( le ` ( F |`s A ) ) z ) ) ) )
39 1 35 38 sylanbrc 
 |-  ( ( F e. Poset /\ A e. V ) -> ( F |`s A ) e. Poset )