This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )