Metamath Proof Explorer

Theorem erinxp

Description: A restricted equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 10-Jul-2015) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypotheses erinxp.r 
|- ( ph -> R Er A )
erinxp.a 
|- ( ph -> B C_ A )
Assertion erinxp 
|- ( ph -> ( R i^i ( B X. B ) ) Er B )

Proof

Step Hyp Ref Expression
1 erinxp.r 
 |-  ( ph -> R Er A )
2 erinxp.a 
 |-  ( ph -> B C_ A )
3 relinxp 
 |-  Rel ( R i^i ( B X. B ) )
4 3 a1i 
 |-  ( ph -> Rel ( R i^i ( B X. B ) ) )
5 simpr 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> x ( R i^i ( B X. B ) ) y )
6 brinxp2 
 |-  ( x ( R i^i ( B X. B ) ) y <-> ( ( x e. B /\ y e. B ) /\ x R y ) )
7 5 6 sylib 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> ( ( x e. B /\ y e. B ) /\ x R y ) )
8 7 simplrd 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> y e. B )
9 7 simplld 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> x e. B )
10 1 adantr 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> R Er A )
11 7 simprd 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> x R y )
12 10 11 ersym 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> y R x )
13 brinxp2 
 |-  ( y ( R i^i ( B X. B ) ) x <-> ( ( y e. B /\ x e. B ) /\ y R x ) )
14 8 9 12 13 syl21anbrc 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> y ( R i^i ( B X. B ) ) x )
15 9 adantrr 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> x e. B )
16 simprr 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> y ( R i^i ( B X. B ) ) z )
17 brinxp2 
 |-  ( y ( R i^i ( B X. B ) ) z <-> ( ( y e. B /\ z e. B ) /\ y R z ) )
18 16 17 sylib 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> ( ( y e. B /\ z e. B ) /\ y R z ) )
19 18 simplrd 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> z e. B )
20 1 adantr 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> R Er A )
21 11 adantrr 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> x R y )
22 18 simprd 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> y R z )
23 20 21 22 ertrd 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> x R z )
24 brinxp2 
 |-  ( x ( R i^i ( B X. B ) ) z <-> ( ( x e. B /\ z e. B ) /\ x R z ) )
25 15 19 23 24 syl21anbrc 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> x ( R i^i ( B X. B ) ) z )
26 1 adantr 
 |-  ( ( ph /\ x e. B ) -> R Er A )
27 2 sselda 
 |-  ( ( ph /\ x e. B ) -> x e. A )
28 26 27 erref 
 |-  ( ( ph /\ x e. B ) -> x R x )
29 28 ex 
 |-  ( ph -> ( x e. B -> x R x ) )
30 29 pm4.71rd 
 |-  ( ph -> ( x e. B <-> ( x R x /\ x e. B ) ) )
31 brin 
 |-  ( x ( R i^i ( B X. B ) ) x <-> ( x R x /\ x ( B X. B ) x ) )
32 brxp 
 |-  ( x ( B X. B ) x <-> ( x e. B /\ x e. B ) )
33 anidm 
 |-  ( ( x e. B /\ x e. B ) <-> x e. B )
34 32 33 bitri 
 |-  ( x ( B X. B ) x <-> x e. B )
35 34 anbi2i 
 |-  ( ( x R x /\ x ( B X. B ) x ) <-> ( x R x /\ x e. B ) )
36 31 35 bitri 
 |-  ( x ( R i^i ( B X. B ) ) x <-> ( x R x /\ x e. B ) )
37 30 36 bitr4di 
 |-  ( ph -> ( x e. B <-> x ( R i^i ( B X. B ) ) x ) )
38 4 14 25 37 iserd 
 |-  ( ph -> ( R i^i ( B X. B ) ) Er B )