# Metamath Proof Explorer

## Theorem asymref2

Description: Two ways of saying a relation is antisymmetric and reflexive. (Contributed by NM, 6-May-2008) (Proof shortened by Mario Carneiro, 4-Dec-2016)

Ref Expression
Assertion asymref2 ${⊢}{R}\cap {{R}}^{-1}={\mathrm{I}↾}_{\bigcup \bigcup {R}}↔\left(\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}{x}{R}{x}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 asymref ${⊢}{R}\cap {{R}}^{-1}={\mathrm{I}↾}_{\bigcup \bigcup {R}}↔\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)↔{x}={y}\right)$
2 albiim ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)↔{x}={y}\right)↔\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)\right)$
3 2 ralbii ${⊢}\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)↔{x}={y}\right)↔\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)\right)$
4 r19.26 ${⊢}\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)\right)↔\left(\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\wedge \forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)\right)$
5 ancom ${⊢}\left(\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\wedge \forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)\right)↔\left(\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)\wedge \forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)$
6 equcom ${⊢}{x}={y}↔{y}={x}$
7 6 imbi1i ${⊢}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)↔\left({y}={x}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)$
8 7 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)$
9 breq2 ${⊢}{y}={x}\to \left({x}{R}{y}↔{x}{R}{x}\right)$
10 breq1 ${⊢}{y}={x}\to \left({y}{R}{x}↔{x}{R}{x}\right)$
11 9 10 anbi12d ${⊢}{y}={x}\to \left(\left({x}{R}{y}\wedge {y}{R}{x}\right)↔\left({x}{R}{x}\wedge {x}{R}{x}\right)\right)$
12 anidm ${⊢}\left({x}{R}{x}\wedge {x}{R}{x}\right)↔{x}{R}{x}$
13 11 12 syl6bb ${⊢}{y}={x}\to \left(\left({x}{R}{y}\wedge {y}{R}{x}\right)↔{x}{R}{x}\right)$
14 13 equsalvw ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)↔{x}{R}{x}$
15 8 14 bitri ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)↔{x}{R}{x}$
16 15 ralbii ${⊢}\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)↔\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}{x}{R}{x}$
17 df-ral ${⊢}\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \bigcup \bigcup {R}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)$
18 df-br ${⊢}{x}{R}{y}↔⟨{x},{y}⟩\in {R}$
19 vex ${⊢}{x}\in \mathrm{V}$
20 vex ${⊢}{y}\in \mathrm{V}$
21 19 20 opeluu ${⊢}⟨{x},{y}⟩\in {R}\to \left({x}\in \bigcup \bigcup {R}\wedge {y}\in \bigcup \bigcup {R}\right)$
22 21 simpld ${⊢}⟨{x},{y}⟩\in {R}\to {x}\in \bigcup \bigcup {R}$
23 18 22 sylbi ${⊢}{x}{R}{y}\to {x}\in \bigcup \bigcup {R}$
24 23 adantr ${⊢}\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}\in \bigcup \bigcup {R}$
25 24 pm2.24d ${⊢}\left({x}{R}{y}\wedge {y}{R}{x}\right)\to \left(¬{x}\in \bigcup \bigcup {R}\to {x}={y}\right)$
26 25 com12 ${⊢}¬{x}\in \bigcup \bigcup {R}\to \left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)$
27 26 alrimiv ${⊢}¬{x}\in \bigcup \bigcup {R}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)$
28 id ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)$
29 27 28 ja ${⊢}\left({x}\in \bigcup \bigcup {R}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)$
30 ax-1 ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\to \left({x}\in \bigcup \bigcup {R}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)$
31 29 30 impbii ${⊢}\left({x}\in \bigcup \bigcup {R}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)$
32 31 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \bigcup \bigcup {R}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)$
33 17 32 bitri ${⊢}\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)$
34 16 33 anbi12i ${⊢}\left(\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)\wedge \forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)↔\left(\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}{x}{R}{x}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)$
35 4 5 34 3bitri ${⊢}\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to \left({x}{R}{y}\wedge {y}{R}{x}\right)\right)\right)↔\left(\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}{x}{R}{x}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)$
36 1 3 35 3bitri ${⊢}{R}\cap {{R}}^{-1}={\mathrm{I}↾}_{\bigcup \bigcup {R}}↔\left(\forall {x}\in \bigcup \bigcup {R}\phantom{\rule{.4em}{0ex}}{x}{R}{x}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}{R}{y}\wedge {y}{R}{x}\right)\to {x}={y}\right)\right)$