Metamath Proof Explorer

Theorem ressprs

Description: The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015)

Ref Expression
Hypothesis ressprs.b 
|- B = ( Base ` K )
Assertion ressprs 
|- ( ( K e. Proset /\ A C_ B ) -> ( K |`s A ) e. Proset )

Proof

Step Hyp Ref Expression
1 ressprs.b 
 |-  B = ( Base ` K )
2 ovexd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( K |`s A ) e. _V )
3 simp-4l 
 |-  ( ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) /\ z e. A ) -> K e. Proset )
4 simp-4r 
 |-  ( ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) /\ z e. A ) -> A C_ B )
5 simpllr 
 |-  ( ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) /\ z e. A ) -> x e. A )
6 4 5 sseldd 
 |-  ( ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) /\ z e. A ) -> x e. B )
7 3 6 jca 
 |-  ( ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) /\ z e. A ) -> ( K e. Proset /\ x e. B ) )
8 simplr 
 |-  ( ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) /\ z e. A ) -> y e. A )
9 4 8 sseldd 
 |-  ( ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) /\ z e. A ) -> y e. B )
10 simpr 
 |-  ( ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) /\ z e. A ) -> z e. A )
11 4 10 sseldd 
 |-  ( ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) /\ z e. A ) -> z e. B )
12 eqid 
 |-  ( le ` K ) = ( le ` K )
13 1 12 isprs 
 |-  ( K e. Proset <-> ( K e. _V /\ A. x e. B A. y e. B A. z e. B ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) )
14 13 simprbi 
 |-  ( K e. Proset -> A. x e. B A. y e. B A. z e. B ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
15 14 r19.21bi 
 |-  ( ( K e. Proset /\ x e. B ) -> A. y e. B A. z e. B ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
16 15 r19.21bi 
 |-  ( ( ( K e. Proset /\ x e. B ) /\ y e. B ) -> A. z e. B ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
17 16 r19.21bi 
 |-  ( ( ( ( K e. Proset /\ x e. B ) /\ y e. B ) /\ z e. B ) -> ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
18 7 9 11 17 syl21anc 
 |-  ( ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) /\ z e. A ) -> ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
19 18 ralrimiva 
 |-  ( ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) /\ y e. A ) -> A. z e. A ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
20 19 ralrimiva 
 |-  ( ( ( K e. Proset /\ A C_ B ) /\ x e. A ) -> A. y e. A A. z e. A ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
21 20 ralrimiva 
 |-  ( ( K e. Proset /\ A C_ B ) -> A. x e. A A. y e. A A. z e. A ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) )
22 eqid 
 |-  ( K |`s A ) = ( K |`s A )
23 22 1 ressbas2 
 |-  ( A C_ B -> A = ( Base ` ( K |`s A ) ) )
24 23 adantl 
 |-  ( ( K e. Proset /\ A C_ B ) -> A = ( Base ` ( K |`s A ) ) )
25 1 fvexi 
 |-  B e. _V
26 25 ssex 
 |-  ( A C_ B -> A e. _V )
27 22 12 ressle 
 |-  ( A e. _V -> ( le ` K ) = ( le ` ( K |`s A ) ) )
28 26 27 syl 
 |-  ( A C_ B -> ( le ` K ) = ( le ` ( K |`s A ) ) )
29 28 adantl 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( le ` K ) = ( le ` ( K |`s A ) ) )
30 29 breqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( x ( le ` K ) x <-> x ( le ` ( K |`s A ) ) x ) )
31 29 breqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( x ( le ` K ) y <-> x ( le ` ( K |`s A ) ) y ) )
32 29 breqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( y ( le ` K ) z <-> y ( le ` ( K |`s A ) ) z ) )
33 31 32 anbi12d 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ( x ( le ` K ) y /\ y ( le ` K ) z ) <-> ( x ( le ` ( K |`s A ) ) y /\ y ( le ` ( K |`s A ) ) z ) ) )
34 29 breqd 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( x ( le ` K ) z <-> x ( le ` ( K |`s A ) ) z ) )
35 33 34 imbi12d 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) <-> ( ( x ( le ` ( K |`s A ) ) y /\ y ( le ` ( K |`s A ) ) z ) -> x ( le ` ( K |`s A ) ) z ) ) )
36 30 35 anbi12d 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) <-> ( x ( le ` ( K |`s A ) ) x /\ ( ( x ( le ` ( K |`s A ) ) y /\ y ( le ` ( K |`s A ) ) z ) -> x ( le ` ( K |`s A ) ) z ) ) ) )
37 24 36 raleqbidv 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( A. z e. A ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) <-> A. z e. ( Base ` ( K |`s A ) ) ( x ( le ` ( K |`s A ) ) x /\ ( ( x ( le ` ( K |`s A ) ) y /\ y ( le ` ( K |`s A ) ) z ) -> x ( le ` ( K |`s A ) ) z ) ) ) )
38 24 37 raleqbidv 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( A. y e. A A. z e. A ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) <-> A. y e. ( Base ` ( K |`s A ) ) A. z e. ( Base ` ( K |`s A ) ) ( x ( le ` ( K |`s A ) ) x /\ ( ( x ( le ` ( K |`s A ) ) y /\ y ( le ` ( K |`s A ) ) z ) -> x ( le ` ( K |`s A ) ) z ) ) ) )
39 24 38 raleqbidv 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( A. x e. A A. y e. A A. z e. A ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) <-> A. x e. ( Base ` ( K |`s A ) ) A. y e. ( Base ` ( K |`s A ) ) A. z e. ( Base ` ( K |`s A ) ) ( x ( le ` ( K |`s A ) ) x /\ ( ( x ( le ` ( K |`s A ) ) y /\ y ( le ` ( K |`s A ) ) z ) -> x ( le ` ( K |`s A ) ) z ) ) ) )
40 39 anbi2d 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ( ( K |`s A ) e. _V /\ A. x e. A A. y e. A A. z e. A ( x ( le ` K ) x /\ ( ( x ( le ` K ) y /\ y ( le ` K ) z ) -> x ( le ` K ) z ) ) ) <-> ( ( K |`s A ) e. _V /\ A. x e. ( Base ` ( K |`s A ) ) A. y e. ( Base ` ( K |`s A ) ) A. z e. ( Base ` ( K |`s A ) ) ( x ( le ` ( K |`s A ) ) x /\ ( ( x ( le ` ( K |`s A ) ) y /\ y ( le ` ( K |`s A ) ) z ) -> x ( le ` ( K |`s A ) ) z ) ) ) ) )
41 2 21 40 mpbi2and 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( ( K |`s A ) e. _V /\ A. x e. ( Base ` ( K |`s A ) ) A. y e. ( Base ` ( K |`s A ) ) A. z e. ( Base ` ( K |`s A ) ) ( x ( le ` ( K |`s A ) ) x /\ ( ( x ( le ` ( K |`s A ) ) y /\ y ( le ` ( K |`s A ) ) z ) -> x ( le ` ( K |`s A ) ) z ) ) ) )
42 eqid 
 |-  ( Base ` ( K |`s A ) ) = ( Base ` ( K |`s A ) )
43 eqid 
 |-  ( le ` ( K |`s A ) ) = ( le ` ( K |`s A ) )
44 42 43 isprs 
 |-  ( ( K |`s A ) e. Proset <-> ( ( K |`s A ) e. _V /\ A. x e. ( Base ` ( K |`s A ) ) A. y e. ( Base ` ( K |`s A ) ) A. z e. ( Base ` ( K |`s A ) ) ( x ( le ` ( K |`s A ) ) x /\ ( ( x ( le ` ( K |`s A ) ) y /\ y ( le ` ( K |`s A ) ) z ) -> x ( le ` ( K |`s A ) ) z ) ) ) )
45 41 44 sylibr 
 |-  ( ( K e. Proset /\ A C_ B ) -> ( K |`s A ) e. Proset )