Metamath Proof Explorer

Theorem brinxper

Description: Conditions for a reflexive, symmetric and transitive binary relation to be an equivalence relation over a class V . (Contributed by AV, 11-Jun-2025)

Ref Expression
Hypotheses brinxper.r 
|- ( x e. V -> x .~ x )
brinxper.s 
|- ( x e. V -> ( x .~ y -> y .~ x ) )
brinxper.t 
|- ( x e. V -> ( ( x .~ y /\ y .~ z ) -> x .~ z ) )
Assertion brinxper 
|- ( .~ i^i ( V X. V ) ) Er V

Proof

Step Hyp Ref Expression
1 brinxper.r 
 |-  ( x e. V -> x .~ x )
2 brinxper.s 
 |-  ( x e. V -> ( x .~ y -> y .~ x ) )
3 brinxper.t 
 |-  ( x e. V -> ( ( x .~ y /\ y .~ z ) -> x .~ z ) )
4 relinxp 
 |-  Rel ( .~ i^i ( V X. V ) )
5 brxp 
 |-  ( x ( V X. V ) y <-> ( x e. V /\ y e. V ) )
6 2 adantr 
 |-  ( ( x e. V /\ y e. V ) -> ( x .~ y -> y .~ x ) )
7 ancom 
 |-  ( ( x e. V /\ y e. V ) <-> ( y e. V /\ x e. V ) )
8 brxp 
 |-  ( y ( V X. V ) x <-> ( y e. V /\ x e. V ) )
9 7 8 sylbb2 
 |-  ( ( x e. V /\ y e. V ) -> y ( V X. V ) x )
10 6 9 jctird 
 |-  ( ( x e. V /\ y e. V ) -> ( x .~ y -> ( y .~ x /\ y ( V X. V ) x ) ) )
11 5 10 sylbi 
 |-  ( x ( V X. V ) y -> ( x .~ y -> ( y .~ x /\ y ( V X. V ) x ) ) )
12 11 impcom 
 |-  ( ( x .~ y /\ x ( V X. V ) y ) -> ( y .~ x /\ y ( V X. V ) x ) )
13 brin 
 |-  ( x ( .~ i^i ( V X. V ) ) y <-> ( x .~ y /\ x ( V X. V ) y ) )
14 brin 
 |-  ( y ( .~ i^i ( V X. V ) ) x <-> ( y .~ x /\ y ( V X. V ) x ) )
15 12 13 14 3imtr4i 
 |-  ( x ( .~ i^i ( V X. V ) ) y -> y ( .~ i^i ( V X. V ) ) x )
16 brin 
 |-  ( y ( .~ i^i ( V X. V ) ) z <-> ( y .~ z /\ y ( V X. V ) z ) )
17 brxp 
 |-  ( y ( V X. V ) z <-> ( y e. V /\ z e. V ) )
18 3 expd 
 |-  ( x e. V -> ( x .~ y -> ( y .~ z -> x .~ z ) ) )
19 18 adantr 
 |-  ( ( x e. V /\ y e. V ) -> ( x .~ y -> ( y .~ z -> x .~ z ) ) )
20 19 impcom 
 |-  ( ( x .~ y /\ ( x e. V /\ y e. V ) ) -> ( y .~ z -> x .~ z ) )
21 20 com12 
 |-  ( y .~ z -> ( ( x .~ y /\ ( x e. V /\ y e. V ) ) -> x .~ z ) )
22 21 adantl 
 |-  ( ( ( y e. V /\ z e. V ) /\ y .~ z ) -> ( ( x .~ y /\ ( x e. V /\ y e. V ) ) -> x .~ z ) )
23 22 imp 
 |-  ( ( ( ( y e. V /\ z e. V ) /\ y .~ z ) /\ ( x .~ y /\ ( x e. V /\ y e. V ) ) ) -> x .~ z )
24 simplr 
 |-  ( ( ( y e. V /\ z e. V ) /\ y .~ z ) -> z e. V )
25 simprl 
 |-  ( ( x .~ y /\ ( x e. V /\ y e. V ) ) -> x e. V )
26 24 25 anim12ci 
 |-  ( ( ( ( y e. V /\ z e. V ) /\ y .~ z ) /\ ( x .~ y /\ ( x e. V /\ y e. V ) ) ) -> ( x e. V /\ z e. V ) )
27 23 26 jca 
 |-  ( ( ( ( y e. V /\ z e. V ) /\ y .~ z ) /\ ( x .~ y /\ ( x e. V /\ y e. V ) ) ) -> ( x .~ z /\ ( x e. V /\ z e. V ) ) )
28 27 exp31 
 |-  ( ( y e. V /\ z e. V ) -> ( y .~ z -> ( ( x .~ y /\ ( x e. V /\ y e. V ) ) -> ( x .~ z /\ ( x e. V /\ z e. V ) ) ) ) )
29 17 28 sylbi 
 |-  ( y ( V X. V ) z -> ( y .~ z -> ( ( x .~ y /\ ( x e. V /\ y e. V ) ) -> ( x .~ z /\ ( x e. V /\ z e. V ) ) ) ) )
30 29 impcom 
 |-  ( ( y .~ z /\ y ( V X. V ) z ) -> ( ( x .~ y /\ ( x e. V /\ y e. V ) ) -> ( x .~ z /\ ( x e. V /\ z e. V ) ) ) )
31 5 anbi2i 
 |-  ( ( x .~ y /\ x ( V X. V ) y ) <-> ( x .~ y /\ ( x e. V /\ y e. V ) ) )
32 brxp 
 |-  ( x ( V X. V ) z <-> ( x e. V /\ z e. V ) )
33 32 anbi2i 
 |-  ( ( x .~ z /\ x ( V X. V ) z ) <-> ( x .~ z /\ ( x e. V /\ z e. V ) ) )
34 30 31 33 3imtr4g 
 |-  ( ( y .~ z /\ y ( V X. V ) z ) -> ( ( x .~ y /\ x ( V X. V ) y ) -> ( x .~ z /\ x ( V X. V ) z ) ) )
35 16 34 sylbi 
 |-  ( y ( .~ i^i ( V X. V ) ) z -> ( ( x .~ y /\ x ( V X. V ) y ) -> ( x .~ z /\ x ( V X. V ) z ) ) )
36 35 com12 
 |-  ( ( x .~ y /\ x ( V X. V ) y ) -> ( y ( .~ i^i ( V X. V ) ) z -> ( x .~ z /\ x ( V X. V ) z ) ) )
37 13 36 sylbi 
 |-  ( x ( .~ i^i ( V X. V ) ) y -> ( y ( .~ i^i ( V X. V ) ) z -> ( x .~ z /\ x ( V X. V ) z ) ) )
38 37 imp 
 |-  ( ( x ( .~ i^i ( V X. V ) ) y /\ y ( .~ i^i ( V X. V ) ) z ) -> ( x .~ z /\ x ( V X. V ) z ) )
39 brin 
 |-  ( x ( .~ i^i ( V X. V ) ) z <-> ( x .~ z /\ x ( V X. V ) z ) )
40 38 39 sylibr 
 |-  ( ( x ( .~ i^i ( V X. V ) ) y /\ y ( .~ i^i ( V X. V ) ) z ) -> x ( .~ i^i ( V X. V ) ) z )
41 id 
 |-  ( x e. V -> x e. V )
42 brxp 
 |-  ( x ( V X. V ) x <-> ( x e. V /\ x e. V ) )
43 41 41 42 sylanbrc 
 |-  ( x e. V -> x ( V X. V ) x )
44 1 43 jca 
 |-  ( x e. V -> ( x .~ x /\ x ( V X. V ) x ) )
45 42 simplbi 
 |-  ( x ( V X. V ) x -> x e. V )
46 45 adantl 
 |-  ( ( x .~ x /\ x ( V X. V ) x ) -> x e. V )
47 44 46 impbii 
 |-  ( x e. V <-> ( x .~ x /\ x ( V X. V ) x ) )
48 brin 
 |-  ( x ( .~ i^i ( V X. V ) ) x <-> ( x .~ x /\ x ( V X. V ) x ) )
49 47 48 bitr4i 
 |-  ( x e. V <-> x ( .~ i^i ( V X. V ) ) x )
50 4 15 40 49 iseri 
 |-  ( .~ i^i ( V X. V ) ) Er V