Theorem sonr 5598

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2146   class class class wbr 5114   Po wpo 5572   Or wor 5573

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-po 5574  df-so 5575

This theorem is used by:  sotric  5604  sotrieq  5605  soirri  6131  suppr  9442  infpr  9475  hartogslem1  9514  canth4  10650  canthwelem  10653  pwfseqlem4  10665  1ne0sr  11099  ltnr  11323  opsrtoslem2  22244  nodenselem4  27888  nodenselem5  27889  nodenselem7  27891  nolt02o  27896  nogt01o  27897  noresle  27898  nosupbnd1lem1  27909  nosupbnd2lem1  27916  noinfbnd1lem1  27924  noinfbnd2lem1  27931  ltsirr  27947  weiunpo  37017  fin2solem  38298  fin2so  38299