Theorem ontr2 3889

Description: Transitive law for ordinal numbers. Exercise 3 of [TakeutiZaring] p. 40.

Assertion

Ref	Expression
ontr2	|- ((A e. On /\ C e. On) -> ((A C_ B /\ B e. C) -> A e. C))

Proof of Theorem ontr2

Step	Hyp	Ref	Expression
1		eloni 3853	. 2 |- (A e. On -> Ord A)
2		eloni 3853	. 2 |- (C e. On -> Ord C)
3		ordtr2 3887	. 2 |- ((Ord A /\ Ord C) -> ((A C_ B /\ B e. C) -> A e. C))
4	1, 2, 3	syl2an 699	1 |- ((A e. On /\ C e. On) -> ((A C_ B /\ B e. C) -> A e. C))

Syntax hints:   -> wi 3   /\ wa 433   e. wcel 1617   C_ wss 2859  Ord word 3842  Oncon0 3843

This theorem is referenced by:  smoge 5321  oeordsuc 5475  omxpenlem 5712  rankxplim 6124  infxpenlem 6212  omsubindss 6244  alephle 6278  alephleOLD 6279  pwcfsdom 6527  omopthlem2 14749  axfelem6 14951  omsubindssOLD 16482  smogeOLD 17537

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847

Copyright terms: Public domain