Theorem sonr 5582

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2144   class class class wbr 5102   Po wpo 5556   Or wor 5557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-po 5558  df-so 5559

This theorem is used by:  sotric  5588  sotrieq  5589  soirri  6119  suppr  9467  infpr  9500  hartogslem1  9539  canth4  10735  canthwelem  10738  pwfseqlem4  10750  1ne0sr  11184  ltnr  11408  opsrtoslem2  22370  nodenselem4  28049  nodenselem5  28050  nodenselem7  28052  nolt02o  28057  nogt01o  28058  noresle  28059  nosupbnd1lem1  28070  nosupbnd2lem1  28077  noinfbnd1lem1  28085  noinfbnd2lem1  28092  ltsirr  28108  weiunpo  37345  fin2solem  38622  fin2so  38623