Theorem sonr 5613

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2099   class class class wbr 5148   Po wpo 5588   Or wor 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149  df-po 5590  df-so 5591

This theorem is referenced by:  sotric  5618  sotrieq  5619  soirri  6132  suppr  9494  infpr  9526  hartogslem1  9565  canth4  10670  canthwelem  10673  pwfseqlem4  10685  1ne0sr  11119  ltnr  11339  opsrtoslem2  21999  nodenselem4  27619  nodenselem5  27620  nodenselem7  27622  nolt02o  27627  nogt01o  27628  noresle  27629  nosupbnd1lem1  27640  nosupbnd2lem1  27647  noinfbnd1lem1  27655  noinfbnd2lem1  27662  sltirr  27678  fin2solem  37079  fin2so  37080