![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ordtr | GIF version |
Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
ordtr | ⊢ (Ord 𝐴 → Tr 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dford3 4104 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) | |
2 | 1 | simplbi 259 | 1 ⊢ (Ord 𝐴 → Tr 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wral 2306 Tr wtr 3854 Ord word 4099 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 df-iord 4103 |
This theorem is referenced by: ordelss 4116 ordin 4122 ordtr1 4125 orduniss 4162 ontrci 4164 ordon 4212 ordsucim 4226 ordsucss 4230 onsucsssucr 4235 onintonm 4243 ordsucunielexmid 4256 ordn2lp 4269 onsucuni2 4288 nlimsucg 4290 ordpwsucss 4291 tfrexlem 5948 |
Copyright terms: Public domain | W3C validator |