Theorem issod 5593

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ w3o 1102   ∈ wcel 2144  ∀wral 3076   class class class wbr 5102   Po wpo 5556   Or wor 5557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077  df-so 5559

This theorem is used by:  issoi  5594  swoso  8756  wemapsolem  9548  chnso  18804  legso  29068  weiunso  37347  fin2so  38624