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 brinxp2 
 |-  ( x ( R i^i ( B X. B ) ) y <-> ( ( x e. B /\ y e. B ) /\ x R y ) )
6 5 bilani 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> ( ( x e. B /\ y e. B ) /\ x R y ) )
7 6 simplrd 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> y e. B )
8 6 simplld 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> x e. B )
9 1 adantr 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> R Er A )
10 6 simprd 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> x R y )
11 9 10 ersym 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> y R x )
12 brinxp2 
 |-  ( y ( R i^i ( B X. B ) ) x <-> ( ( y e. B /\ x e. B ) /\ y R x ) )
13 7 8 11 12 syl21anbrc 
 |-  ( ( ph /\ x ( R i^i ( B X. B ) ) y ) -> y ( R i^i ( B X. B ) ) x )
14 8 adantrr 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> x e. B )
15 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 )
16 brinxp2 
 |-  ( y ( R i^i ( B X. B ) ) z <-> ( ( y e. B /\ z e. B ) /\ y R z ) )
17 15 16 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 ) )
18 17 simplrd 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> z e. B )
19 1 adantr 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> R Er A )
20 10 adantrr 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> x R y )
21 17 simprd 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> y R z )
22 19 20 21 ertrd 
 |-  ( ( ph /\ ( x ( R i^i ( B X. B ) ) y /\ y ( R i^i ( B X. B ) ) z ) ) -> x R z )
23 brinxp2 
 |-  ( x ( R i^i ( B X. B ) ) z <-> ( ( x e. B /\ z e. B ) /\ x R z ) )
24 14 18 22 23 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 )
25 1 adantr 
 |-  ( ( ph /\ x e. B ) -> R Er A )
26 2 sselda 
 |-  ( ( ph /\ x e. B ) -> x e. A )
27 25 26 erref 
 |-  ( ( ph /\ x e. B ) -> x R x )
28 27 ex 
 |-  ( ph -> ( x e. B -> x R x ) )
29 28 pm4.71rd 
 |-  ( ph -> ( x e. B <-> ( x R x /\ x e. B ) ) )
30 brin 
 |-  ( x ( R i^i ( B X. B ) ) x <-> ( x R x /\ x ( B X. B ) x ) )
31 brxp 
 |-  ( x ( B X. B ) x <-> ( x e. B /\ x e. B ) )
32 anidm 
 |-  ( ( x e. B /\ x e. B ) <-> x e. B )
33 31 32 bitri 
 |-  ( x ( B X. B ) x <-> x e. B )
34 33 anbi2i 
 |-  ( ( x R x /\ x ( B X. B ) x ) <-> ( x R x /\ x e. B ) )
35 30 34 bitri 
 |-  ( x ( R i^i ( B X. B ) ) x <-> ( x R x /\ x e. B ) )
36 29 35 bitr4di 
 |-  ( ph -> ( x e. B <-> x ( R i^i ( B X. B ) ) x ) )
37 4 13 24 36 iserd 
 |-  ( ph -> ( R i^i ( B X. B ) ) Er B )