Metamath Proof Explorer


Theorem dftr6

Description: A potential definition of transitivity for sets. (Contributed by Scott Fenton, 18-Mar-2012)

Ref Expression
Hypothesis dftr6.1
|- A e. _V
Assertion dftr6
|- ( Tr A <-> A e. ( _V \ ran ( ( _E o. _E ) \ _E ) ) )

Proof

Step Hyp Ref Expression
1 dftr6.1
 |-  A e. _V
2 1 elrn
 |-  ( A e. ran ( ( _E o. _E ) \ _E ) <-> E. x x ( ( _E o. _E ) \ _E ) A )
3 brdif
 |-  ( x ( ( _E o. _E ) \ _E ) A <-> ( x ( _E o. _E ) A /\ -. x _E A ) )
4 vex
 |-  x e. _V
5 4 1 brco
 |-  ( x ( _E o. _E ) A <-> E. y ( x _E y /\ y _E A ) )
6 epel
 |-  ( x _E y <-> x e. y )
7 1 epeli
 |-  ( y _E A <-> y e. A )
8 6 7 anbi12i
 |-  ( ( x _E y /\ y _E A ) <-> ( x e. y /\ y e. A ) )
9 8 exbii
 |-  ( E. y ( x _E y /\ y _E A ) <-> E. y ( x e. y /\ y e. A ) )
10 5 9 bitri
 |-  ( x ( _E o. _E ) A <-> E. y ( x e. y /\ y e. A ) )
11 1 epeli
 |-  ( x _E A <-> x e. A )
12 11 notbii
 |-  ( -. x _E A <-> -. x e. A )
13 10 12 anbi12i
 |-  ( ( x ( _E o. _E ) A /\ -. x _E A ) <-> ( E. y ( x e. y /\ y e. A ) /\ -. x e. A ) )
14 19.41v
 |-  ( E. y ( ( x e. y /\ y e. A ) /\ -. x e. A ) <-> ( E. y ( x e. y /\ y e. A ) /\ -. x e. A ) )
15 exanali
 |-  ( E. y ( ( x e. y /\ y e. A ) /\ -. x e. A ) <-> -. A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
16 14 15 bitr3i
 |-  ( ( E. y ( x e. y /\ y e. A ) /\ -. x e. A ) <-> -. A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
17 3 13 16 3bitri
 |-  ( x ( ( _E o. _E ) \ _E ) A <-> -. A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
18 17 exbii
 |-  ( E. x x ( ( _E o. _E ) \ _E ) A <-> E. x -. A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
19 exnal
 |-  ( E. x -. A. y ( ( x e. y /\ y e. A ) -> x e. A ) <-> -. A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
20 2 18 19 3bitri
 |-  ( A e. ran ( ( _E o. _E ) \ _E ) <-> -. A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
21 20 con2bii
 |-  ( A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) <-> -. A e. ran ( ( _E o. _E ) \ _E ) )
22 dftr2
 |-  ( Tr A <-> A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) )
23 eldif
 |-  ( A e. ( _V \ ran ( ( _E o. _E ) \ _E ) ) <-> ( A e. _V /\ -. A e. ran ( ( _E o. _E ) \ _E ) ) )
24 1 23 mpbiran
 |-  ( A e. ( _V \ ran ( ( _E o. _E ) \ _E ) ) <-> -. A e. ran ( ( _E o. _E ) \ _E ) )
25 21 22 24 3bitr4i
 |-  ( Tr A <-> A e. ( _V \ ran ( ( _E o. _E ) \ _E ) ) )