Theorem sonr 5573

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5110   Po wpo 5547   Or wor 5548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-po 5549  df-so 5550

This theorem is referenced by:  sotric  5579  sotrieq  5580  soirri  6102  suppr  9430  infpr  9463  hartogslem1  9502  canth4  10607  canthwelem  10610  pwfseqlem4  10622  1ne0sr  11056  ltnr  11276  opsrtoslem2  21970  nodenselem4  27606  nodenselem5  27607  nodenselem7  27609  nolt02o  27614  nogt01o  27615  noresle  27616  nosupbnd1lem1  27627  nosupbnd2lem1  27634  noinfbnd1lem1  27642  noinfbnd2lem1  27649  sltirr  27665  weiunpo  36460  fin2solem  37607  fin2so  37608