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 Proset A B K 𝑠 A Proset

Proof

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