ordsson - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ordsson		Structured version Visualization version GIF version

Theorem ordsson 7525

Description: Any ordinal class is a subclass of the class of ordinal numbers. Corollary 7.15 of [TakeutiZaring] p. 38. (Contributed by NM, 18-May-1994.) (Proof shortened by Andrew Salmon, 12-Aug-2011.)

**Assertion**
Ref	Expression
ordsson	⊢ (Ord 𝐴 → 𝐴 ⊆ On)

**Proof of Theorem ordsson**
Step	Hyp	Ref	Expression
1		ordon 7519	. 2 ⊢ Ord On
2		ordeleqon 7524	. . . . 5 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	biimpi 219	. . . 4 ⊢ (Ord 𝐴 → (𝐴 ∈ On ∨ 𝐴 = On))
4	3	adantr 484	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
5		ordsseleq 6201	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ⊆ On ↔ (𝐴 ∈ On ∨ 𝐴 = On)))
6	4, 5	mpbird 260	. 2 ⊢ ((Ord 𝐴 ∧ Ord On) → 𝐴 ⊆ On)
7	1, 6	mpan2 691	1 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∨ wo 846 = wceq 1542 ∈ wcel 2114 ⊆ wss 3843 Ord word 6171 Oncon0 6172

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-11 2162 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pr 5296 ax-un 7481

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-pss 3862 df-nul 4212 df-if 4415 df-sn 4517 df-pr 4519 df-tp 4521 df-op 4523 df-uni 4797 df-br 5031 df-opab 5093 df-tr 5137 df-eprel 5434 df-po 5442 df-so 5443 df-fr 5483 df-we 5485 df-ord 6175 df-on 6176

This theorem is referenced by: onss 7526 orduni 7530 ordsucuniel 7560 ordsucuni 7565 iordsmo 8025 dfrecs3 8040 tfr2b 8063 tz7.44-2 8074 ordiso2 9054 ordtypelem7 9063 ordtypelem8 9064 oiid 9080 r1tr 9280 r1ordg 9282 r1ord3g 9283 r1pwss 9288 r1val1 9290 rankwflemb 9297 r1elwf 9300 rankr1ai 9302 cflim2 9765 cfss 9767 cfslb 9768 cfslbn 9769 cfslb2n 9770 cofsmo 9771 coftr 9775 inaprc 10338 satfn 32890 dford5 33246 rdgprc 33346 nosepon 33513 limsucncmpi 34279

W3C validator