Theorem sonr 5577

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2141   class class class wbr 5099   Po wpo 5551   Or wor 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-po 5553  df-so 5554

This theorem is referenced by:  sotric  5583  sotrieq  5584  soirri  6110  suppr  9415  infpr  9448  hartogslem1  9487  canth4  10602  canthwelem  10605  pwfseqlem4  10617  1ne0sr  11051  ltnr  11275  opsrtoslem2  22089  nodenselem4  27728  nodenselem5  27729  nodenselem7  27731  nolt02o  27736  nogt01o  27737  noresle  27738  nosupbnd1lem1  27749  nosupbnd2lem1  27756  noinfbnd1lem1  27764  noinfbnd2lem1  27771  ltsirr  27787  weiunpo  36789  fin2solem  38069  fin2so  38070