Theorem ontr2 6213

Description: Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Nov-2003.)

Assertion

Ref	Expression
ontr2	⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))

Proof of Theorem ontr2

Step	Hyp	Ref	Expression
1		eloni 6176	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6176	. 2 ⊢ (𝐶 ∈ On → Ord 𝐶)
3		ordtr2 6210	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐶) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
4	1, 2, 3	syl2an 599	1 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2113   ⊆ wss 3841  Ord word 6165  Oncon0 6166

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 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293

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-nf 1791  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-tr 5134  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-ord 6169  df-on 6170

This theorem is referenced by:  oeordsuc  8244  oelimcl  8250  oeeui  8252  omopthlem2  8307  omxpenlem  8660  oismo  9070  cantnflem1c  9216  cantnflem1  9218  cantnflem3  9220  rankr1ai  9293  rankxplim  9374  infxpenlem  9506  alephle  9581  pwcfsdom  10076  r1limwun  10229  onelssex  33226  onunel  33255  naddssim  33470  oldbdayim  33701  ontopbas  34247  ontgval  34250