Theorem ontri1 6225

Description: A trichotomy law for ordinal numbers. (Contributed by NM, 6-Nov-2003.)

Assertion

Ref	Expression
ontri1	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

Proof of Theorem ontri1

Step	Hyp	Ref	Expression
1		eloni 6201	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6201	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6224	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
4	1, 2, 3	syl2an 597	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∈ wcel 2114   ⊆ wss 3936  Ord word 6190  Oncon0 6191

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-tr 5173  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-ord 6194  df-on 6195

This theorem is referenced by:  oneqmini  6242  onmindif  6280  onint  7510  onnmin  7518  onmindif2  7527  dfom2  7582  ondif2  8127  oaword  8175  oawordeulem  8180  oaf1o  8189  odi  8205  omeulem1  8208  oeeulem  8227  oeeui  8228  nnmword  8259  domtriord  8663  sdomel  8664  onsdominel  8666  ordunifi  8768  cantnfp1lem3  9143  oemapvali  9147  cantnflem1b  9149  cantnflem1  9152  cnfcom3lem  9166  rankr1clem  9249  rankelb  9253  rankval3b  9255  rankr1a  9265  unbndrank  9271  rankxplim3  9310  cardne  9394  carden2b  9396  cardsdomel  9403  carddom2  9406  harcard  9407  domtri2  9418  infxpenlem  9439  alephord  9501  alephord3  9504  alephle  9514  dfac12k  9573  cflim2  9685  cofsmo  9691  cfsmolem  9692  isf32lem5  9779  pwcfsdom  10005  pwfseqlem3  10082  inar1  10197  om2uzlt2i  13320  sltval2  33163  sltres  33169  nosepssdm  33190  nolt02olem  33198  nolt02o  33199  noetalem3  33219  nocvxminlem  33247  onsuct0  33789  onint1  33797  ontric3g  39908  infordmin  39919  alephiso3  39938