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 7154

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 7147	. 2 ⊢ Ord On
2		ordeleqon 7153	. . . . 5 ⊢ (Ord 𝐴 ↔ (𝐴 ∈ On ∨ 𝐴 = On))
3	2	biimpi 206	. . . 4 ⊢ (Ord 𝐴 → (𝐴 ∈ On ∨ 𝐴 = On))
4	3	adantr 472	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ∈ On ∨ 𝐴 = On))
5		ordsseleq 5913	. . 3 ⊢ ((Ord 𝐴 ∧ Ord On) → (𝐴 ⊆ On ↔ (𝐴 ∈ On ∨ 𝐴 = On)))
6	4, 5	mpbird 247	. 2 ⊢ ((Ord 𝐴 ∧ Ord On) → 𝐴 ⊆ On)
7	1, 6	mpan2 709	1 ⊢ (Ord 𝐴 → 𝐴 ⊆ On)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∨ wo 382 ∧ wa 383 = wceq 1632 ∈ wcel 2139 ⊆ wss 3715 Ord word 5883 Oncon0 5884

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pr 5055 ax-un 7114

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ne 2933 df-ral 3055 df-rex 3056 df-rab 3059 df-v 3342 df-sbc 3577 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-pss 3731 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-tp 4326 df-op 4328 df-uni 4589 df-br 4805 df-opab 4865 df-tr 4905 df-eprel 5179 df-po 5187 df-so 5188 df-fr 5225 df-we 5227 df-ord 5887 df-on 5888

This theorem is referenced by: onss 7155 orduni 7159 ordsucuniel 7189 ordsucuni 7194 iordsmo 7623 dfrecs3 7638 tfr2b 7661 tz7.44-2 7672 ordiso2 8585 ordtypelem7 8594 ordtypelem8 8595 oiid 8611 r1tr 8812 r1ordg 8814 r1ord3g 8815 r1pwss 8820 r1val1 8822 rankwflemb 8829 r1elwf 8832 rankr1ai 8834 cflim2 9277 cfss 9279 cfslb 9280 cfslbn 9281 cfslb2n 9282 cofsmo 9283 coftr 9287 inaprc 9850 dford5 31915 rdgprc 32005 nosepon 32124 limsucncmpi 32750

W3C validator