Theorem ontr2 6363

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 6325	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6325	. 2 ⊢ (𝐶 ∈ On → Ord 𝐶)
3		ordtr2 6360	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐶) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))
4	1, 2, 3	syl2an 596	1 ⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3899  Ord word 6314  Oncon0 6315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-ord 6318  df-on 6319

This theorem is referenced by:  onelssex  6364  onunel  6422  oeordsuc  8520  oelimcl  8526  oeeui  8528  omopthlem2  8586  coflton  8597  cofon1  8598  cofon2  8599  naddssim  8611  omxpenlem  9004  oismo  9443  cantnflem1c  9594  cantnflem1  9596  cantnflem3  9598  rankr1ai  9708  rankxplim  9789  infxpenlem  9921  alephle  9996  pwcfsdom  10492  r1limwun  10645  oldbdayim  27861  addsbdaylem  27986  negsbdaylem  28025  onscutlt  28232  ontopbas  36571  ontgval  36574  onexlimgt  43427  nnoeomeqom  43496  omabs2  43516  oaun3lem2  43559  nadd2rabex  43570  nadd1suc  43576