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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
Assertion ressprs ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐾 ↾s 𝐴 ) ∈ Proset )

Proof

Step Hyp Ref Expression
1 ressprs.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ovexd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐾 ↾s 𝐴 ) ∈ V )
3 simp-4l ⊢ ( ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝐾 ∈ Proset )
4 simp-4r ⊢ ( ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝐴 ⊆ 𝐵 )
5 simpllr ⊢ ( ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
6 4 5 sseldd ⊢ ( ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
7 3 6 jca ⊢ ( ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝐾 ∈ Proset ∧ 𝑥 ∈ 𝐵 ) )
8 simplr ⊢ ( ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
9 4 8 sseldd ⊢ ( ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 )
10 simpr ⊢ ( ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
11 4 10 sseldd ⊢ ( ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐵 )
12 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
13 1 12 isprs ⊢ ( 𝐾 ∈ Proset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
14 13 simprbi ⊢ ( 𝐾 ∈ Proset → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
15 14 r19.21bi ⊢ ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ 𝐵 ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
16 15 r19.21bi ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ∀ 𝑧 ∈ 𝐵 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
17 16 r19.21bi ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
18 7 9 11 17 syl21anc ⊢ ( ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
19 18 ralrimiva ⊢ ( ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
20 19 ralrimiva ⊢ ( ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
21 20 ralrimiva ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
22 eqid ⊢ ( 𝐾 ↾s 𝐴 ) = ( 𝐾 ↾s 𝐴 )
23 22 1 ressbas2 ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
24 23 adantl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → 𝐴 = ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) )
25 1 fvexi ⊢ 𝐵 ∈ V
26 25 ssex ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ∈ V )
27 22 12 ressle ⊢ ( 𝐴 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾 ↾s 𝐴 ) ) )
28 26 27 syl ⊢ ( 𝐴 ⊆ 𝐵 → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾 ↾s 𝐴 ) ) )
29 28 adantl ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾 ↾s 𝐴 ) ) )
30 29 breqd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ↔ 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑥 ) )
31 29 breqd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑦 ) )
32 29 breqd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑦 ( le ‘ 𝐾 ) 𝑧 ↔ 𝑦 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) )
33 31 32 anbi12d ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) ↔ ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) ) )
34 29 breqd ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑧 ↔ 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) )
35 33 34 imbi12d ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ↔ ( ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) ) )
36 30 35 anbi12d ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) ) ) )
37 24 36 raleqbidv ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) ) ) )
38 24 37 raleqbidv ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) ) ) )
39 24 38 raleqbidv ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) ) ) )
40 39 anbi2d ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ( ( 𝐾 ↾s 𝐴 ) ∈ V ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( 𝑥 ( le ‘ 𝐾 ) 𝑥 ∧ ( ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ 𝑦 ( le ‘ 𝐾 ) 𝑧 ) → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ↔ ( ( 𝐾 ↾s 𝐴 ) ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) ) ) ) )
41 2 21 40 mpbi2and ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝐾 ↾s 𝐴 ) ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) ) ) )
42 eqid ⊢ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) = ( Base ‘ ( 𝐾 ↾s 𝐴 ) )
43 eqid ⊢ ( le ‘ ( 𝐾 ↾s 𝐴 ) ) = ( le ‘ ( 𝐾 ↾s 𝐴 ) )
44 42 43 isprs ⊢ ( ( 𝐾 ↾s 𝐴 ) ∈ Proset ↔ ( ( 𝐾 ↾s 𝐴 ) ∈ V ∧ ∀ 𝑥 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ∀ 𝑦 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ∀ 𝑧 ∈ ( Base ‘ ( 𝐾 ↾s 𝐴 ) ) ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑥 ∧ ( ( 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑦 ∧ 𝑦 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) → 𝑥 ( le ‘ ( 𝐾 ↾s 𝐴 ) ) 𝑧 ) ) ) )
45 41 44 sylibr ⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐾 ↾s 𝐴 ) ∈ Proset )