Theorem sonr 5526

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2106   class class class wbr 5074   Po wpo 5501   Or wor 5502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-po 5503  df-so 5504

This theorem is referenced by:  sotric  5531  sotrieq  5532  soirri  6031  suppr  9230  infpr  9262  hartogslem1  9301  canth4  10403  canthwelem  10406  pwfseqlem4  10418  1ne0sr  10852  ltnr  11070  opsrtoslem2  21263  nodenselem4  33890  nodenselem5  33891  nodenselem7  33893  nolt02o  33898  nogt01o  33899  noresle  33900  nosupbnd1lem1  33911  nosupbnd2lem1  33918  noinfbnd1lem1  33926  noinfbnd2lem1  33933  sltirr  33949  fin2solem  35763  fin2so  35764