Theorem sonr 5632

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5166   Po wpo 5605   Or wor 5606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-po 5607  df-so 5608

This theorem is referenced by:  sotric  5637  sotrieq  5638  soirri  6158  suppr  9540  infpr  9572  hartogslem1  9611  canth4  10716  canthwelem  10719  pwfseqlem4  10731  1ne0sr  11165  ltnr  11385  opsrtoslem2  22103  nodenselem4  27750  nodenselem5  27751  nodenselem7  27753  nolt02o  27758  nogt01o  27759  noresle  27760  nosupbnd1lem1  27771  nosupbnd2lem1  27778  noinfbnd1lem1  27786  noinfbnd2lem1  27793  sltirr  27809  weiunpo  36431  fin2solem  37566  fin2so  37567