Theorem sonr 5572

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5109   Po wpo 5546   Or wor 5547

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-ext 2702

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-po 5548  df-so 5549

This theorem is referenced by:  sotric  5578  sotrieq  5579  soirri  6101  suppr  9429  infpr  9462  hartogslem1  9501  canth4  10606  canthwelem  10609  pwfseqlem4  10621  1ne0sr  11055  ltnr  11275  opsrtoslem2  21969  nodenselem4  27605  nodenselem5  27606  nodenselem7  27608  nolt02o  27613  nogt01o  27614  noresle  27615  nosupbnd1lem1  27626  nosupbnd2lem1  27633  noinfbnd1lem1  27641  noinfbnd2lem1  27648  sltirr  27664  weiunpo  36448  fin2solem  37595  fin2so  37596