Theorem sonr 5595

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2143   class class class wbr 5110   Po wpo 5569   Or wor 5570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-po 5571  df-so 5572

This theorem is referenced by:  sotric  5601  sotrieq  5602  soirri  6128  suppr  9433  infpr  9466  hartogslem1  9505  canth4  10633  canthwelem  10636  pwfseqlem4  10648  1ne0sr  11082  ltnr  11306  opsrtoslem2  22188  nodenselem4  27832  nodenselem5  27833  nodenselem7  27835  nolt02o  27840  nogt01o  27841  noresle  27842  nosupbnd1lem1  27853  nosupbnd2lem1  27860  noinfbnd1lem1  27868  noinfbnd2lem1  27875  ltsirr  27891  weiunpo  36957  fin2solem  38238  fin2so  38239