Theorem sonr 5469

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2111   class class class wbr 5036   Po wpo 5445   Or wor 5446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-v 3411  df-un 3865  df-sn 4526  df-pr 4528  df-op 4532  df-br 5037  df-po 5447  df-so 5448

This theorem is referenced by:  sotric  5474  sotrieq  5475  soirri  5963  suppr  8981  infpr  9013  hartogslem1  9052  canth4  10120  canthwelem  10123  pwfseqlem4  10135  1ne0sr  10569  ltnr  10786  opsrtoslem2  20829  nodenselem4  33487  nodenselem5  33488  nodenselem7  33490  nolt02o  33495  nogt01o  33496  noresle  33497  nosupbnd1lem1  33508  nosupbnd2lem1  33515  noinfbnd1lem1  33523  noinfbnd2lem1  33530  sltirr  33546  fin2solem  35357  fin2so  35358