Theorem sonr 5583

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 5578	. 2 ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴)
2		poirr 5571	. 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 5103   Po wpo 5557   Or wor 5558

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-po 5559  df-so 5560

This theorem is used by:  sotric  5589  sotrieq  5590  soirri  6118  suppr  9448  infpr  9481  hartogslem1  9520  canth4  10713  canthwelem  10716  pwfseqlem4  10728  1ne0sr  11162  ltnr  11386  opsrtoslem2  22345  nodenselem4  28026  nodenselem5  28027  nodenselem7  28029  nolt02o  28034  nogt01o  28035  noresle  28036  nosupbnd1lem1  28047  nosupbnd2lem1  28054  noinfbnd1lem1  28062  noinfbnd2lem1  28069  ltsirr  28085  weiunpo  37223  fin2solem  38497  fin2so  38498