Theorem sonr 5594

Description: A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)

Assertion

Ref	Expression
sonr	⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)

Proof of Theorem sonr

Step	Hyp	Ref	Expression
1		sopo 5589	. 2 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
2		poirr 5582	. 2 ⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
3	1, 2	sylan 591	1 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2149   class class class wbr 5113   Po wpo 5568   Or wor 5569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-po 5570  df-so 5571

This theorem is referenced by:  sotric  5600  sotrieq  5601  soirri  6127  suppr  9432  infpr  9465  hartogslem1  9504  canth4  10632  canthwelem  10635  pwfseqlem4  10647  1ne0sr  11081  ltnr  11305  opsrtoslem2  22176  nodenselem4  27817  nodenselem5  27818  nodenselem7  27820  nolt02o  27825  nogt01o  27826  noresle  27827  nosupbnd1lem1  27838  nosupbnd2lem1  27845  noinfbnd1lem1  27853  noinfbnd2lem1  27860  ltsirr  27876  weiunpo  36899  fin2solem  38179  fin2so  38180