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 ∧ ∀ 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