![]() |
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 4297 | . 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) | |
2 | 1 | simplbi 272 | 1 ⊢ (Ord 𝐴 → Tr 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wral 2417 Tr wtr 4034 Ord word 4292 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-iord 4296 |
This theorem is referenced by: ordelss 4309 ordin 4315 ordtr1 4318 orduniss 4355 ontrci 4357 ordon 4410 ordsucim 4424 ordsucss 4428 onsucsssucr 4433 onintonm 4441 ordsucunielexmid 4454 ordn2lp 4468 onsucuni2 4487 nlimsucg 4489 ordpwsucss 4490 tfrexlem 6239 nnsucuniel 6399 ctmlemr 7001 nnnninf 7031 ctinf 11979 nnsf 13374 peano4nninf 13375 nninfalllemn 13377 |
Copyright terms: Public domain | W3C validator |