MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brinxper Structured version   Visualization version   GIF version

Theorem brinxper 8772
Description: Conditions for a reflexive, symmetric and transitive binary relation to be an equivalence relation over a class 𝑉. (Contributed by AV, 11-Jun-2025.)
Hypotheses
Ref Expression
brinxper.r (𝑥𝑉𝑥 𝑥)
brinxper.s (𝑥𝑉 → (𝑥 𝑦𝑦 𝑥))
brinxper.t (𝑥𝑉 → ((𝑥 𝑦𝑦 𝑧) → 𝑥 𝑧))
Assertion
Ref Expression
brinxper ( ∩ (𝑉 × 𝑉)) Er 𝑉
Distinct variable groups:   𝑥,𝑉,𝑦,𝑧   𝑥, ,𝑦,𝑧

Proof of Theorem brinxper
StepHypRef Expression
1 relinxp 5826 . 2 Rel ( ∩ (𝑉 × 𝑉))
2 brxp 5737 . . . . 5 (𝑥(𝑉 × 𝑉)𝑦 ↔ (𝑥𝑉𝑦𝑉))
3 brinxper.s . . . . . . 7 (𝑥𝑉 → (𝑥 𝑦𝑦 𝑥))
43adantr 480 . . . . . 6 ((𝑥𝑉𝑦𝑉) → (𝑥 𝑦𝑦 𝑥))
5 ancom 460 . . . . . . 7 ((𝑥𝑉𝑦𝑉) ↔ (𝑦𝑉𝑥𝑉))
6 brxp 5737 . . . . . . 7 (𝑦(𝑉 × 𝑉)𝑥 ↔ (𝑦𝑉𝑥𝑉))
75, 6sylbb2 238 . . . . . 6 ((𝑥𝑉𝑦𝑉) → 𝑦(𝑉 × 𝑉)𝑥)
84, 7jctird 526 . . . . 5 ((𝑥𝑉𝑦𝑉) → (𝑥 𝑦 → (𝑦 𝑥𝑦(𝑉 × 𝑉)𝑥)))
92, 8sylbi 217 . . . 4 (𝑥(𝑉 × 𝑉)𝑦 → (𝑥 𝑦 → (𝑦 𝑥𝑦(𝑉 × 𝑉)𝑥)))
109impcom 407 . . 3 ((𝑥 𝑦𝑥(𝑉 × 𝑉)𝑦) → (𝑦 𝑥𝑦(𝑉 × 𝑉)𝑥))
11 brin 5199 . . 3 (𝑥( ∩ (𝑉 × 𝑉))𝑦 ↔ (𝑥 𝑦𝑥(𝑉 × 𝑉)𝑦))
12 brin 5199 . . 3 (𝑦( ∩ (𝑉 × 𝑉))𝑥 ↔ (𝑦 𝑥𝑦(𝑉 × 𝑉)𝑥))
1310, 11, 123imtr4i 292 . 2 (𝑥( ∩ (𝑉 × 𝑉))𝑦𝑦( ∩ (𝑉 × 𝑉))𝑥)
14 brin 5199 . . . . . . 7 (𝑦( ∩ (𝑉 × 𝑉))𝑧 ↔ (𝑦 𝑧𝑦(𝑉 × 𝑉)𝑧))
15 brxp 5737 . . . . . . . . . 10 (𝑦(𝑉 × 𝑉)𝑧 ↔ (𝑦𝑉𝑧𝑉))
16 brinxper.t . . . . . . . . . . . . . . . . . 18 (𝑥𝑉 → ((𝑥 𝑦𝑦 𝑧) → 𝑥 𝑧))
1716expd 415 . . . . . . . . . . . . . . . . 17 (𝑥𝑉 → (𝑥 𝑦 → (𝑦 𝑧𝑥 𝑧)))
1817adantr 480 . . . . . . . . . . . . . . . 16 ((𝑥𝑉𝑦𝑉) → (𝑥 𝑦 → (𝑦 𝑧𝑥 𝑧)))
1918impcom 407 . . . . . . . . . . . . . . 15 ((𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉)) → (𝑦 𝑧𝑥 𝑧))
2019com12 32 . . . . . . . . . . . . . 14 (𝑦 𝑧 → ((𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉)) → 𝑥 𝑧))
2120adantl 481 . . . . . . . . . . . . 13 (((𝑦𝑉𝑧𝑉) ∧ 𝑦 𝑧) → ((𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉)) → 𝑥 𝑧))
2221imp 406 . . . . . . . . . . . 12 ((((𝑦𝑉𝑧𝑉) ∧ 𝑦 𝑧) ∧ (𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉))) → 𝑥 𝑧)
23 simplr 769 . . . . . . . . . . . . 13 (((𝑦𝑉𝑧𝑉) ∧ 𝑦 𝑧) → 𝑧𝑉)
24 simprl 771 . . . . . . . . . . . . 13 ((𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉)) → 𝑥𝑉)
2523, 24anim12ci 614 . . . . . . . . . . . 12 ((((𝑦𝑉𝑧𝑉) ∧ 𝑦 𝑧) ∧ (𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉))) → (𝑥𝑉𝑧𝑉))
2622, 25jca 511 . . . . . . . . . . 11 ((((𝑦𝑉𝑧𝑉) ∧ 𝑦 𝑧) ∧ (𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉))) → (𝑥 𝑧 ∧ (𝑥𝑉𝑧𝑉)))
2726exp31 419 . . . . . . . . . 10 ((𝑦𝑉𝑧𝑉) → (𝑦 𝑧 → ((𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉)) → (𝑥 𝑧 ∧ (𝑥𝑉𝑧𝑉)))))
2815, 27sylbi 217 . . . . . . . . 9 (𝑦(𝑉 × 𝑉)𝑧 → (𝑦 𝑧 → ((𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉)) → (𝑥 𝑧 ∧ (𝑥𝑉𝑧𝑉)))))
2928impcom 407 . . . . . . . 8 ((𝑦 𝑧𝑦(𝑉 × 𝑉)𝑧) → ((𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉)) → (𝑥 𝑧 ∧ (𝑥𝑉𝑧𝑉))))
302anbi2i 623 . . . . . . . 8 ((𝑥 𝑦𝑥(𝑉 × 𝑉)𝑦) ↔ (𝑥 𝑦 ∧ (𝑥𝑉𝑦𝑉)))
31 brxp 5737 . . . . . . . . 9 (𝑥(𝑉 × 𝑉)𝑧 ↔ (𝑥𝑉𝑧𝑉))
3231anbi2i 623 . . . . . . . 8 ((𝑥 𝑧𝑥(𝑉 × 𝑉)𝑧) ↔ (𝑥 𝑧 ∧ (𝑥𝑉𝑧𝑉)))
3329, 30, 323imtr4g 296 . . . . . . 7 ((𝑦 𝑧𝑦(𝑉 × 𝑉)𝑧) → ((𝑥 𝑦𝑥(𝑉 × 𝑉)𝑦) → (𝑥 𝑧𝑥(𝑉 × 𝑉)𝑧)))
3414, 33sylbi 217 . . . . . 6 (𝑦( ∩ (𝑉 × 𝑉))𝑧 → ((𝑥 𝑦𝑥(𝑉 × 𝑉)𝑦) → (𝑥 𝑧𝑥(𝑉 × 𝑉)𝑧)))
3534com12 32 . . . . 5 ((𝑥 𝑦𝑥(𝑉 × 𝑉)𝑦) → (𝑦( ∩ (𝑉 × 𝑉))𝑧 → (𝑥 𝑧𝑥(𝑉 × 𝑉)𝑧)))
3611, 35sylbi 217 . . . 4 (𝑥( ∩ (𝑉 × 𝑉))𝑦 → (𝑦( ∩ (𝑉 × 𝑉))𝑧 → (𝑥 𝑧𝑥(𝑉 × 𝑉)𝑧)))
3736imp 406 . . 3 ((𝑥( ∩ (𝑉 × 𝑉))𝑦𝑦( ∩ (𝑉 × 𝑉))𝑧) → (𝑥 𝑧𝑥(𝑉 × 𝑉)𝑧))
38 brin 5199 . . 3 (𝑥( ∩ (𝑉 × 𝑉))𝑧 ↔ (𝑥 𝑧𝑥(𝑉 × 𝑉)𝑧))
3937, 38sylibr 234 . 2 ((𝑥( ∩ (𝑉 × 𝑉))𝑦𝑦( ∩ (𝑉 × 𝑉))𝑧) → 𝑥( ∩ (𝑉 × 𝑉))𝑧)
40 brinxper.r . . . . 5 (𝑥𝑉𝑥 𝑥)
41 id 22 . . . . . 6 (𝑥𝑉𝑥𝑉)
42 brxp 5737 . . . . . 6 (𝑥(𝑉 × 𝑉)𝑥 ↔ (𝑥𝑉𝑥𝑉))
4341, 41, 42sylanbrc 583 . . . . 5 (𝑥𝑉𝑥(𝑉 × 𝑉)𝑥)
4440, 43jca 511 . . . 4 (𝑥𝑉 → (𝑥 𝑥𝑥(𝑉 × 𝑉)𝑥))
4542simplbi 497 . . . . 5 (𝑥(𝑉 × 𝑉)𝑥𝑥𝑉)
4645adantl 481 . . . 4 ((𝑥 𝑥𝑥(𝑉 × 𝑉)𝑥) → 𝑥𝑉)
4744, 46impbii 209 . . 3 (𝑥𝑉 ↔ (𝑥 𝑥𝑥(𝑉 × 𝑉)𝑥))
48 brin 5199 . . 3 (𝑥( ∩ (𝑉 × 𝑉))𝑥 ↔ (𝑥 𝑥𝑥(𝑉 × 𝑉)𝑥))
4947, 48bitr4i 278 . 2 (𝑥𝑉𝑥( ∩ (𝑉 × 𝑉))𝑥)
501, 13, 39, 49iseri 8770 1 ( ∩ (𝑉 × 𝑉)) Er 𝑉
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2105  cin 3961   class class class wbr 5147   × cxp 5686   Er wer 8740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-er 8743
This theorem is referenced by:  gricer  47830  grlicer  47911
  Copyright terms: Public domain W3C validator