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∈Ax∈y∨x=y∨y∈x

Proof

Step Hyp Ref Expression
1 df-ord ⊢Ord⁡A↔Tr⁡A∧EWeA
2 zfregfr ⊢EFrA
3 dfwe2 ⊢EWeA↔EFrA∧∀x∈A∀y∈AxEy∨x=y∨yEx
4 2 3 mpbiran ⊢EWeA↔∀x∈A∀y∈AxEy∨x=y∨yEx
5 epel ⊢xEy↔x∈y
6 biid ⊢x=y↔x=y
7 epel ⊢yEx↔y∈x
8 5 6 7 3orbi123i ⊢xEy∨x=y∨yEx↔x∈y∨x=y∨y∈x
9 8 2ralbii ⊢∀x∈A∀y∈AxEy∨x=y∨yEx↔∀x∈A∀y∈Ax∈y∨x=y∨y∈x
10 4 9 bitri ⊢EWeA↔∀x∈A∀y∈Ax∈y∨x=y∨y∈x
11 10 anbi2i ⊢Tr⁡A∧EWeA↔Tr⁡A∧∀x∈A∀y∈Ax∈y∨x=y∨y∈x
12 1 11 bitri ⊢Ord⁡A↔Tr⁡A∧∀x∈A∀y∈Ax∈y∨x=y∨y∈x