Description: Given ax-reg , an ordinal is a transitive class totally ordered by the membership relation. (Contributed by Scott Fenton, 28-Jan-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | dford5reg | ⊢ ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ E Or 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ord | ⊢ ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ E We 𝐴 ) ) | |
2 | zfregfr | ⊢ E Fr 𝐴 | |
3 | df-we | ⊢ ( E We 𝐴 ↔ ( E Fr 𝐴 ∧ E Or 𝐴 ) ) | |
4 | 2 3 | mpbiran | ⊢ ( E We 𝐴 ↔ E Or 𝐴 ) |
5 | 4 | anbi2i | ⊢ ( ( Tr 𝐴 ∧ E We 𝐴 ) ↔ ( Tr 𝐴 ∧ E Or 𝐴 ) ) |
6 | 1 5 | bitri | ⊢ ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ E Or 𝐴 ) ) |