Theorem ontri1 6100

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 6076	. 2 ⊢ (𝐴 ∈ On → Ord 𝐴)
2		eloni 6076	. 2 ⊢ (𝐵 ∈ On → Ord 𝐵)
3		ordtri1 6099	. 2 ⊢ ((Ord 𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))
4	1, 2, 3	syl2an 595	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2081   ⊆ wss 3859  Ord word 6065  Oncon0 6066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-pss 3876  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-tr 5064  df-eprel 5353  df-po 5362  df-so 5363  df-fr 5402  df-we 5404  df-ord 6069  df-on 6070

This theorem is referenced by:  oneqmini  6117  onmindif  6155  onint  7366  onnmin  7374  onmindif2  7383  dfom2  7438  ondif2  7978  oaword  8025  oawordeulem  8030  oaf1o  8039  odi  8055  omeulem1  8058  oeeulem  8077  oeeui  8078  nnmword  8109  domtriord  8510  sdomel  8511  onsdominel  8513  ordunifi  8614  cantnfp1lem3  8989  oemapvali  8993  cantnflem1b  8995  cantnflem1  8998  cnfcom3lem  9012  rankr1clem  9095  rankelb  9099  rankval3b  9101  rankr1a  9111  unbndrank  9117  rankxplim3  9156  cardne  9240  carden2b  9242  cardsdomel  9249  carddom2  9252  harcard  9253  domtri2  9264  infxpenlem  9285  alephord  9347  alephord3  9350  alephle  9360  dfac12k  9419  cflim2  9531  cofsmo  9537  cfsmolem  9538  isf32lem5  9625  pwcfsdom  9851  pwfseqlem3  9928  inar1  10043  om2uzlt2i  13169  sltval2  32772  sltres  32778  nosepssdm  32799  nolt02olem  32807  nolt02o  32808  noetalem3  32828  nocvxminlem  32856  onsuct0  33398  onint1  33406  ontric3g  39373  infordmin  39384  alephiso3  39403