Theorem sonr 5557

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2119   class class class wbr 5079   Po wpo 5531   Or wor 5532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-po 5533  df-so 5534

This theorem is referenced by:  sotric  5563  sotrieq  5564  soirri  6083  suppr  9382  infpr  9415  hartogslem1  9454  canth4  10568  canthwelem  10571  pwfseqlem4  10583  1ne0sr  11017  ltnr  11239  opsrtoslem2  22039  nodenselem4  27676  nodenselem5  27677  nodenselem7  27679  nolt02o  27684  nogt01o  27685  noresle  27686  nosupbnd1lem1  27697  nosupbnd2lem1  27704  noinfbnd1lem1  27712  noinfbnd2lem1  27719  ltsirr  27735  weiunpo  36700  fin2solem  37980  fin2so  37981