Theorem sonr 5585

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 5580	. 2 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
2		poirr 5573	. 2 ⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)
3	1, 2	sylan 580	1 ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5119   Po wpo 5559   Or wor 5560

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-po 5561  df-so 5562

This theorem is referenced by:  sotric  5591  sotrieq  5592  soirri  6115  suppr  9484  infpr  9517  hartogslem1  9556  canth4  10661  canthwelem  10664  pwfseqlem4  10676  1ne0sr  11110  ltnr  11330  opsrtoslem2  22014  nodenselem4  27651  nodenselem5  27652  nodenselem7  27654  nolt02o  27659  nogt01o  27660  noresle  27661  nosupbnd1lem1  27672  nosupbnd2lem1  27679  noinfbnd1lem1  27687  noinfbnd2lem1  27694  sltirr  27710  weiunpo  36483  fin2solem  37630  fin2so  37631