Metamath Proof Explorer


Theorem opeldifid

Description: Ordered pair elementhood outside of the diagonal. (Contributed by Thierry Arnoux, 1-Jan-2020)

Ref Expression
Assertion opeldifid
|- ( Rel A -> ( <. X , Y >. e. ( A \ _I ) <-> ( <. X , Y >. e. A /\ X =/= Y ) ) )

Proof

Step Hyp Ref Expression
1 reldif
 |-  ( Rel A -> Rel ( A \ _I ) )
2 brrelex2
 |-  ( ( Rel ( A \ _I ) /\ X ( A \ _I ) Y ) -> Y e. _V )
3 1 2 sylan
 |-  ( ( Rel A /\ X ( A \ _I ) Y ) -> Y e. _V )
4 brrelex2
 |-  ( ( Rel A /\ X A Y ) -> Y e. _V )
5 4 adantrr
 |-  ( ( Rel A /\ ( X A Y /\ X =/= Y ) ) -> Y e. _V )
6 brdif
 |-  ( X ( A \ _I ) Y <-> ( X A Y /\ -. X _I Y ) )
7 ideqg
 |-  ( Y e. _V -> ( X _I Y <-> X = Y ) )
8 7 necon3bbid
 |-  ( Y e. _V -> ( -. X _I Y <-> X =/= Y ) )
9 8 anbi2d
 |-  ( Y e. _V -> ( ( X A Y /\ -. X _I Y ) <-> ( X A Y /\ X =/= Y ) ) )
10 6 9 syl5bb
 |-  ( Y e. _V -> ( X ( A \ _I ) Y <-> ( X A Y /\ X =/= Y ) ) )
11 3 5 10 pm5.21nd
 |-  ( Rel A -> ( X ( A \ _I ) Y <-> ( X A Y /\ X =/= Y ) ) )
12 df-br
 |-  ( X ( A \ _I ) Y <-> <. X , Y >. e. ( A \ _I ) )
13 df-br
 |-  ( X A Y <-> <. X , Y >. e. A )
14 13 anbi1i
 |-  ( ( X A Y /\ X =/= Y ) <-> ( <. X , Y >. e. A /\ X =/= Y ) )
15 11 12 14 3bitr3g
 |-  ( Rel A -> ( <. X , Y >. e. ( A \ _I ) <-> ( <. X , Y >. e. A /\ X =/= Y ) ) )