Theorem ontr2 6432

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   ⊆ wss 3962  Ord word 6384  Oncon0 6385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-tr 5265  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-ord 6388  df-on 6389

This theorem is referenced by:  onelssex  6433  onunel  6490  oeordsuc  8630  oelimcl  8636  oeeui  8638  omopthlem2  8696  coflton  8707  cofon1  8708  cofon2  8709  naddssim  8721  omxpenlem  9111  oismo  9577  cantnflem1c  9724  cantnflem1  9726  cantnflem3  9728  rankr1ai  9835  rankxplim  9916  infxpenlem  10050  alephle  10125  pwcfsdom  10620  r1limwun  10773  oldbdayim  27941  addsbdaylem  28063  negsbdaylem  28102  ontopbas  36410  ontgval  36413  onexlimgt  43231  nnoeomeqom  43301  omabs2  43321  oaun3lem2  43364  nadd2rabex  43375  nadd1suc  43381