Theorem sonr 5591

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145   class class class wbr 5107   Po wpo 5565   Or wor 5566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-po 5567  df-so 5568

This theorem is used by:  sotric  5597  sotrieq  5598  soirri  6124  suppr  9446  infpr  9479  hartogslem1  9518  canth4  10660  canthwelem  10663  pwfseqlem4  10675  1ne0sr  11109  ltnr  11333  opsrtoslem2  22278  nodenselem4  27931  nodenselem5  27932  nodenselem7  27934  nolt02o  27939  nogt01o  27940  noresle  27941  nosupbnd1lem1  27952  nosupbnd2lem1  27959  noinfbnd1lem1  27967  noinfbnd2lem1  27974  ltsirr  27990  weiunpo  37092  fin2solem  38368  fin2so  38369