Theorem domnsym 9118

Description: Theorem 22(i) of [Suppes] p. 97. (Contributed by NM, 10-Jun-1998.)

Assertion

Ref	Expression
domnsym	⊢ (𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴)

Proof of Theorem domnsym

Step	Hyp	Ref	Expression
1		brdom2 9001	. 2 ⊢ (𝐴 ≼ 𝐵 ↔ (𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵))
2		sdomnsym 9117	. . 3 ⊢ (𝐴 ≺ 𝐵 → ¬ 𝐵 ≺ 𝐴)
3		sdomnen 9000	. . . 4 ⊢ (𝐵 ≺ 𝐴 → ¬ 𝐵 ≈ 𝐴)
4		ensym 9022	. . . 4 ⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴)
5	3, 4	nsyl3 138	. . 3 ⊢ (𝐴 ≈ 𝐵 → ¬ 𝐵 ≺ 𝐴)
6	2, 5	jaoi 857	. 2 ⊢ ((𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵) → ¬ 𝐵 ≺ 𝐴)
7	1, 6	sylbi 217	1 ⊢ (𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 847   class class class wbr 5124   ≈ cen 8961   ≼ cdom 8962   ≺ csdm 8963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967

This theorem is referenced by:  sdom0OLD  9128  sdomdomtr  9129  domsdomtr  9131  sdomdif  9144  onsdominel  9145  nndomogOLD  9240  sdom1OLD  9256  fofinf1o  9349  carddom2  9996  fidomtri  10012  fidomtri2  10013  infxpenlem  10032  alephordi  10093  infdif  10227  infdif2  10228  cfslbn  10286  cfslb2n  10287  fincssdom  10342  fin45  10411  domtriom  10462  alephval2  10591  alephreg  10601  pwcfsdom  10602  cfpwsdom  10603  pwfseqlem3  10679  gchpwdom  10689  gchaleph  10690  hargch  10692  gchhar  10698  winainflem  10712  rankcf  10796  tskcard  10800  vdwlem12  17017  odinf  19549  rectbntr0  24777  erdszelem10  35227  finminlem  36341  fimgmcyc  42524  fphpd  42806