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 ⊢ ( 𝑥 ∈ 𝑉 → 𝑥 ∼ 𝑥 )
brinxper.s ⊢ ( 𝑥 ∈ 𝑉 → ( 𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥 ) )
brinxper.t ⊢ ( 𝑥 ∈ 𝑉 → ( ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) → 𝑥 ∼ 𝑧 ) )
Assertion brinxper ( ∼ ∩ ( 𝑉 × 𝑉 ) ) Er 𝑉

Proof

Step Hyp Ref Expression
1 brinxper.r ⊢ ( 𝑥 ∈ 𝑉 → 𝑥 ∼ 𝑥 )
2 brinxper.s ⊢ ( 𝑥 ∈ 𝑉 → ( 𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥 ) )
3 brinxper.t ⊢ ( 𝑥 ∈ 𝑉 → ( ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) → 𝑥 ∼ 𝑧 ) )
4 relinxp ⊢ Rel ( ∼ ∩ ( 𝑉 × 𝑉 ) )
5 brxp ⊢ ( 𝑥 ( 𝑉 × 𝑉 ) 𝑦 ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
6 2 adantr ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥 ) )
7 ancom ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ↔ ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) )
8 brxp ⊢ ( 𝑦 ( 𝑉 × 𝑉 ) 𝑥 ↔ ( 𝑦 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) )
9 7 8 sylbb2 ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ( 𝑉 × 𝑉 ) 𝑥 )
10 6 9 jctird ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 ∼ 𝑦 → ( 𝑦 ∼ 𝑥 ∧ 𝑦 ( 𝑉 × 𝑉 ) 𝑥 ) ) )
11 5 10 sylbi ⊢ ( 𝑥 ( 𝑉 × 𝑉 ) 𝑦 → ( 𝑥 ∼ 𝑦 → ( 𝑦 ∼ 𝑥 ∧ 𝑦 ( 𝑉 × 𝑉 ) 𝑥 ) ) )
12 11 impcom ⊢ ( ( 𝑥 ∼ 𝑦 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑦 ) → ( 𝑦 ∼ 𝑥 ∧ 𝑦 ( 𝑉 × 𝑉 ) 𝑥 ) )
13 brin ⊢ ( 𝑥 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑦 ↔ ( 𝑥 ∼ 𝑦 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑦 ) )
14 brin ⊢ ( 𝑦 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑥 ↔ ( 𝑦 ∼ 𝑥 ∧ 𝑦 ( 𝑉 × 𝑉 ) 𝑥 ) )
15 12 13 14 3imtr4i ⊢ ( 𝑥 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑦 → 𝑦 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑥 )
16 brin ⊢ ( 𝑦 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑧 ↔ ( 𝑦 ∼ 𝑧 ∧ 𝑦 ( 𝑉 × 𝑉 ) 𝑧 ) )
17 brxp ⊢ ( 𝑦 ( 𝑉 × 𝑉 ) 𝑧 ↔ ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) )
18 3 expd ⊢ ( 𝑥 ∈ 𝑉 → ( 𝑥 ∼ 𝑦 → ( 𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧 ) ) )
19 18 adantr ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 ∼ 𝑦 → ( 𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧 ) ) )
20 19 impcom ⊢ ( ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧 ) )
21 20 com12 ⊢ ( 𝑦 ∼ 𝑧 → ( ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∼ 𝑧 ) )
22 21 adantl ⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ 𝑦 ∼ 𝑧 ) → ( ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∼ 𝑧 ) )
23 22 imp ⊢ ( ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ 𝑦 ∼ 𝑧 ) ∧ ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ) → 𝑥 ∼ 𝑧 )
24 simplr ⊢ ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ 𝑦 ∼ 𝑧 ) → 𝑧 ∈ 𝑉 )
25 simprl ⊢ ( ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝑥 ∈ 𝑉 )
26 24 25 anim12ci ⊢ ( ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ 𝑦 ∼ 𝑧 ) ∧ ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ) → ( 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) )
27 23 26 jca ⊢ ( ( ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ∧ 𝑦 ∼ 𝑧 ) ∧ ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ) → ( 𝑥 ∼ 𝑧 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) )
28 27 exp31 ⊢ ( ( 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) → ( 𝑦 ∼ 𝑧 → ( ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ∼ 𝑧 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ) ) )
29 17 28 sylbi ⊢ ( 𝑦 ( 𝑉 × 𝑉 ) 𝑧 → ( 𝑦 ∼ 𝑧 → ( ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ∼ 𝑧 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ) ) )
30 29 impcom ⊢ ( ( 𝑦 ∼ 𝑧 ∧ 𝑦 ( 𝑉 × 𝑉 ) 𝑧 ) → ( ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑥 ∼ 𝑧 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) ) )
31 5 anbi2i ⊢ ( ( 𝑥 ∼ 𝑦 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑦 ) ↔ ( 𝑥 ∼ 𝑦 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
32 brxp ⊢ ( 𝑥 ( 𝑉 × 𝑉 ) 𝑧 ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) )
33 32 anbi2i ⊢ ( ( 𝑥 ∼ 𝑧 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑧 ) ↔ ( 𝑥 ∼ 𝑧 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) )
34 30 31 33 3imtr4g ⊢ ( ( 𝑦 ∼ 𝑧 ∧ 𝑦 ( 𝑉 × 𝑉 ) 𝑧 ) → ( ( 𝑥 ∼ 𝑦 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑦 ) → ( 𝑥 ∼ 𝑧 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑧 ) ) )
35 16 34 sylbi ⊢ ( 𝑦 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑧 → ( ( 𝑥 ∼ 𝑦 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑦 ) → ( 𝑥 ∼ 𝑧 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑧 ) ) )
36 35 com12 ⊢ ( ( 𝑥 ∼ 𝑦 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑦 ) → ( 𝑦 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑧 → ( 𝑥 ∼ 𝑧 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑧 ) ) )
37 13 36 sylbi ⊢ ( 𝑥 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑦 → ( 𝑦 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑧 → ( 𝑥 ∼ 𝑧 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑧 ) ) )
38 37 imp ⊢ ( ( 𝑥 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑦 ∧ 𝑦 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑧 ) → ( 𝑥 ∼ 𝑧 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑧 ) )
39 brin ⊢ ( 𝑥 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑧 ↔ ( 𝑥 ∼ 𝑧 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑧 ) )
40 38 39 sylibr ⊢ ( ( 𝑥 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑦 ∧ 𝑦 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑧 ) → 𝑥 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑧 )
41 id ⊢ ( 𝑥 ∈ 𝑉 → 𝑥 ∈ 𝑉 )
42 brxp ⊢ ( 𝑥 ( 𝑉 × 𝑉 ) 𝑥 ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉 ) )
43 41 41 42 sylanbrc ⊢ ( 𝑥 ∈ 𝑉 → 𝑥 ( 𝑉 × 𝑉 ) 𝑥 )
44 1 43 jca ⊢ ( 𝑥 ∈ 𝑉 → ( 𝑥 ∼ 𝑥 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑥 ) )
45 42 simplbi ⊢ ( 𝑥 ( 𝑉 × 𝑉 ) 𝑥 → 𝑥 ∈ 𝑉 )
46 45 adantl ⊢ ( ( 𝑥 ∼ 𝑥 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑥 ) → 𝑥 ∈ 𝑉 )
47 44 46 impbii ⊢ ( 𝑥 ∈ 𝑉 ↔ ( 𝑥 ∼ 𝑥 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑥 ) )
48 brin ⊢ ( 𝑥 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑥 ↔ ( 𝑥 ∼ 𝑥 ∧ 𝑥 ( 𝑉 × 𝑉 ) 𝑥 ) )
49 47 48 bitr4i ⊢ ( 𝑥 ∈ 𝑉 ↔ 𝑥 ( ∼ ∩ ( 𝑉 × 𝑉 ) ) 𝑥 )
50 4 15 40 49 iseri ⊢ ( ∼ ∩ ( 𝑉 × 𝑉 ) ) Er 𝑉