Theorem issod 5594

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 3208	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))
4		df-so 5560	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5	1, 3, 4	sylanbrc 594	1 ⊢ (𝜑 → 𝑅 Or 𝐴)

Syntax hints:   → wi 4   ∧ wa 400   ∨ w3o 1100   ∈ wcel 2145  ∀wral 3079   class class class wbr 5104   Po wpo 5557   Or wor 5558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3080  df-so 5560

This theorem is referenced by:  issoi  5595  swoso  8717  wemapsolem  9500  chnso  18668  legso  28822  weiunso  36834  fin2so  38113