Theorem dford5 33767

Description: A class is ordinal iff it is a subclass of On and transitive. (Contributed by Scott Fenton, 21-Nov-2021.)

Assertion

Ref	Expression
dford5	⊢ (Ord 𝐴 ↔ (𝐴 ⊆ On ∧ Tr 𝐴))

Proof of Theorem dford5

Step	Hyp	Ref	Expression
1		ordsson 7666	. . 3 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)
2		ordtr 6295	. . 3 ⊢ (Ord 𝐴 → Tr 𝐴)
3	1, 2	jca 512	. 2 ⊢ (Ord 𝐴 → (𝐴 ⊆ On ∧ Tr 𝐴))
4		epweon 7658	. . . 4 ⊢ E We On
5		wess 5587	. . . 4 ⊢ (𝐴 ⊆ On → ( E We On → E We 𝐴))
6	4, 5	mpi 20	. . 3 ⊢ (𝐴 ⊆ On → E We 𝐴)
7		df-ord 6284	. . . . 5 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
8	7	biimpri 227	. . . 4 ⊢ ((Tr 𝐴 ∧ E We 𝐴) → Ord 𝐴)
9	8	ancoms 459	. . 3 ⊢ (( E We 𝐴 ∧ Tr 𝐴) → Ord 𝐴)
10	6, 9	sylan 580	. 2 ⊢ ((𝐴 ⊆ On ∧ Tr 𝐴) → Ord 𝐴)
11	3, 10	impbii 208	1 ⊢ (Ord 𝐴 ↔ (𝐴 ⊆ On ∧ Tr 𝐴))

Syntax hints:   ↔ wb 205   ∧ wa 396   ⊆ wss 3891  Tr wtr 5197   E cep 5505   We wwe 5554  Ord word 6280  Oncon0 6281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-ext 2706  ax-sep 5231  ax-nul 5238  ax-pr 5360

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-sb 2065  df-clab 2713  df-cleq 2727  df-clel 2813  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3357  df-v 3438  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4844  df-br 5081  df-opab 5143  df-tr 5198  df-eprel 5506  df-po 5514  df-so 5515  df-fr 5555  df-we 5557  df-ord 6284  df-on 6285

This theorem is referenced by:  nosupno  33965  noinfno  33980