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

Metamath Proof Explorer

Theorem dford2

Description: Assuming ax-reg , an ordinal is a transitive class on which inclusion satisfies trichotomy. (Contributed by Scott Fenton, 27-Oct-2010)

Ref Expression
Assertion dford2 
|- ( Ord A <-> ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) )

Proof

Step Hyp Ref Expression
1 df-ord 
 |-  ( Ord A <-> ( Tr A /\ _E We A ) )
2 zfregfr 
 |-  _E Fr A
3 dfwe2 
 |-  ( _E We A <-> ( _E Fr A /\ A. x e. A A. y e. A ( x _E y \/ x = y \/ y _E x ) ) )
4 2 3 mpbiran 
 |-  ( _E We A <-> A. x e. A A. y e. A ( x _E y \/ x = y \/ y _E x ) )
5 epel 
 |-  ( x _E y <-> x e. y )
6 biid 
 |-  ( x = y <-> x = y )
7 epel 
 |-  ( y _E x <-> y e. x )
8 5 6 7 3orbi123i 
 |-  ( ( x _E y \/ x = y \/ y _E x ) <-> ( x e. y \/ x = y \/ y e. x ) )
9 8 2ralbii 
 |-  ( A. x e. A A. y e. A ( x _E y \/ x = y \/ y _E x ) <-> A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) )
10 4 9 bitri 
 |-  ( _E We A <-> A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) )
11 10 anbi2i 
 |-  ( ( Tr A /\ _E We A ) <-> ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) )
12 1 11 bitri 
 |-  ( Ord A <-> ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) )