Theorem issod 5627

Description: An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)

Hypotheses

Ref	Expression
issod.1	⊢ (𝜑 → 𝑅 Po 𝐴)
issod.2	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))

Assertion

Ref	Expression
issod	⊢ (𝜑 → 𝑅 Or 𝐴)

Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝐴,𝑦   𝜑,𝑥,𝑦

Proof of Theorem issod

Step	Hyp	Ref	Expression
1		issod.1	. 2 ⊢ (𝜑 → 𝑅 Po 𝐴)
2		issod.2	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
3	2	ralrimivva 3202	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
4		df-so 5593	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5	1, 3, 4	sylanbrc 583	1 ⊢ (𝜑 → 𝑅 Or 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1086   ∈ wcel 2108  ∀wral 3061   class class class wbr 5143   Po wpo 5590   Or wor 5591

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3062  df-so 5593

This theorem is referenced by:  issoi  5628  swoso  8779  wemapsolem  9590  legso  28607  chnso  33004  weiunso  36467  fin2so  37614