Description: A class is ordinal iff it is a subclass of On and transitive. (Contributed by Scott Fenton, 21-Nov-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | dford5 | ⊢ ( Ord 𝐴 ↔ ( 𝐴 ⊆ On ∧ Tr 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordsson | ⊢ ( Ord 𝐴 → 𝐴 ⊆ On ) | |
2 | ordtr | ⊢ ( Ord 𝐴 → Tr 𝐴 ) | |
3 | 1 2 | jca | ⊢ ( Ord 𝐴 → ( 𝐴 ⊆ On ∧ Tr 𝐴 ) ) |
4 | epweon | ⊢ E We On | |
5 | wess | ⊢ ( 𝐴 ⊆ On → ( E We On → E We 𝐴 ) ) | |
6 | 4 5 | mpi | ⊢ ( 𝐴 ⊆ On → E We 𝐴 ) |
7 | df-ord | ⊢ ( Ord 𝐴 ↔ ( Tr 𝐴 ∧ E We 𝐴 ) ) | |
8 | 7 | biimpri | ⊢ ( ( Tr 𝐴 ∧ E We 𝐴 ) → Ord 𝐴 ) |
9 | 8 | ancoms | ⊢ ( ( E We 𝐴 ∧ Tr 𝐴 ) → Ord 𝐴 ) |
10 | 6 9 | sylan | ⊢ ( ( 𝐴 ⊆ On ∧ Tr 𝐴 ) → Ord 𝐴 ) |
11 | 3 10 | impbii | ⊢ ( Ord 𝐴 ↔ ( 𝐴 ⊆ On ∧ Tr 𝐴 ) ) |