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