Metamath Proof Explorer


Theorem untangtr

Description: A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011)

Ref Expression
Assertion untangtr
|- ( Tr A -> ( A. x e. A -. x e. x <-> A. x e. A A. y e. x -. y e. y ) )

Proof

Step Hyp Ref Expression
1 df-tr
 |-  ( Tr A <-> U. A C_ A )
2 ssralv
 |-  ( U. A C_ A -> ( A. x e. A -. x e. x -> A. x e. U. A -. x e. x ) )
3 1 2 sylbi
 |-  ( Tr A -> ( A. x e. A -. x e. x -> A. x e. U. A -. x e. x ) )
4 elequ1
 |-  ( x = y -> ( x e. x <-> y e. x ) )
5 elequ2
 |-  ( x = y -> ( y e. x <-> y e. y ) )
6 4 5 bitrd
 |-  ( x = y -> ( x e. x <-> y e. y ) )
7 6 notbid
 |-  ( x = y -> ( -. x e. x <-> -. y e. y ) )
8 7 cbvralvw
 |-  ( A. x e. U. A -. x e. x <-> A. y e. U. A -. y e. y )
9 untuni
 |-  ( A. y e. U. A -. y e. y <-> A. x e. A A. y e. x -. y e. y )
10 8 9 bitri
 |-  ( A. x e. U. A -. x e. x <-> A. x e. A A. y e. x -. y e. y )
11 3 10 syl6ib
 |-  ( Tr A -> ( A. x e. A -. x e. x -> A. x e. A A. y e. x -. y e. y ) )
12 untelirr
 |-  ( A. y e. x -. y e. y -> -. x e. x )
13 12 ralimi
 |-  ( A. x e. A A. y e. x -. y e. y -> A. x e. A -. x e. x )
14 11 13 impbid1
 |-  ( Tr A -> ( A. x e. A -. x e. x <-> A. x e. A A. y e. x -. y e. y ) )