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 x A y A x y x = y y 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 x A y A x E y x = y y E x
4 2 3 mpbiran E We A x A y A x E y x = y y E x
5 epel x E y x y
6 biid x = y x = y
7 epel y E x y x
8 5 6 7 3orbi123i x E y x = y y E x x y x = y y x
9 8 2ralbii x A y A x E y x = y y E x x A y A x y x = y y x
10 4 9 bitri E We A x A y A x y x = y y x
11 10 anbi2i Tr A E We A Tr A x A y A x y x = y y x
12 1 11 bitri Ord A Tr A x A y A x y x = y y x