Theorem ontr2 6414

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3896  Ord word 6364  Oncon0 6365

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6368  df-on 6369

This theorem is used by:  onelssex  6415  onunel  6473  oeordsuc  8610  oelimcl  8616  oeeui  8618  omopthlem2  8676  coflton  8687  cofon1  8688  cofon2  8689  naddssim  8702  omxpenlem  9104  oismo  9541  cantnflem1c  9695  cantnflem1  9697  cantnflem3  9699  rankr1ai  9813  rankxplim  9903  infxpenlem  10099  alephle  10174  pwcfsdom  10675  r1limwun  10828  oldbdayim  28284  addbdaylem  28412  negbdaylem  28451  oncutlt  28659  maxssj0  35949  ontr2d  37045  ltnmul  37061  ltnadd  37063  ontopbas  37312  ontgval  37315  onexlimgt  44354  nnoeomeqom  44423  omabs2  44443  oaun3lem2  44486  nadd2rabex  44497  nadd1suc  44503