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 φ R Er A
erinxp.a φ B A
Assertion erinxp φ R B × B Er B

Proof

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