Theorem sonr 5570

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5107   Po wpo 5544   Or wor 5545

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-po 5546  df-so 5547

This theorem is referenced by:  sotric  5576  sotrieq  5577  soirri  6099  suppr  9423  infpr  9456  hartogslem1  9495  canth4  10600  canthwelem  10603  pwfseqlem4  10615  1ne0sr  11049  ltnr  11269  opsrtoslem2  21963  nodenselem4  27599  nodenselem5  27600  nodenselem7  27602  nolt02o  27607  nogt01o  27608  noresle  27609  nosupbnd1lem1  27620  nosupbnd2lem1  27627  noinfbnd1lem1  27635  noinfbnd2lem1  27642  sltirr  27658  weiunpo  36453  fin2solem  37600  fin2so  37601