Theorem solin 5573

Description: A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.)

Assertion

Ref	Expression
solin	⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))

Proof of Theorem solin

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 5110	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥𝑅𝑦 ↔ 𝐵𝑅𝑦))
2		eqeq1 2733	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 = 𝑦 ↔ 𝐵 = 𝑦))
3		breq2 5111	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝐵))
4	1, 2, 3	3orbi123d 1437	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝐵𝑅𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦𝑅𝐵)))
5	4	imbi2d 340	. . 3 ⊢ (𝑥 = 𝐵 → ((𝑅 Or 𝐴 → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦𝑅𝐵))))
6		breq2 5111	. . . . 5 ⊢ (𝑦 = 𝐶 → (𝐵𝑅𝑦 ↔ 𝐵𝑅𝐶))
7		eqeq2 2741	. . . . 5 ⊢ (𝑦 = 𝐶 → (𝐵 = 𝑦 ↔ 𝐵 = 𝐶))
8		breq1 5110	. . . . 5 ⊢ (𝑦 = 𝐶 → (𝑦𝑅𝐵 ↔ 𝐶𝑅𝐵))
9	6, 7, 8	3orbi123d 1437	. . . 4 ⊢ (𝑦 = 𝐶 → ((𝐵𝑅𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
10	9	imbi2d 340	. . 3 ⊢ (𝑦 = 𝐶 → ((𝑅 Or 𝐴 → (𝐵𝑅𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦𝑅𝐵)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))))
11		df-so 5547	. . . . 5 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
12		breq1 5110	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥𝑅𝑦 ↔ 𝑧𝑅𝑦))
13		equequ1 2025	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑧 = 𝑦))
14		breq2 5111	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧))
15	12, 13, 14	3orbi123d 1437	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑧𝑅𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦𝑅𝑧)))
16	15	ralbidv 3156	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑧𝑅𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦𝑅𝑧)))
17	16	rspw 3214	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
18		breq2 5111	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑧))
19		equequ2 2026	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧))
20		breq1 5110	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑧𝑅𝑥))
21	18, 19, 20	3orbi123d 1437	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥)))
22	21	rspw 3214	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → (𝑦 ∈ 𝐴 → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
23	17, 22	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
24	23	impd 410	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
25	11, 24	simplbiim 504	. . . 4 ⊢ (𝑅 Or 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
26	25	com12 32	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑅 Or 𝐴 → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
27	5, 10, 26	vtocl2ga 3544	. 2 ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝑅 Or 𝐴 → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
28	27	impcom 407	1 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085   = wceq 1540   ∈ wcel 2109  ∀wral 3044   class class class wbr 5107   Po wpo 5544   Or wor 5545

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-so 5547

This theorem is referenced by:  sotric  5576  sotrieq  5577  somo  5585  wecmpep  5630  sorpssi  7705  soxp  8108  infsupprpr  9457  wemaplem2  9500  fpwwe2lem11  10594  fpwwe2lem12  10595  lttri4  11258  xmullem  13224  xmulasslem  13245  noresle  27609  nosupbnd1lem6  27625  noinfbnd1lem6  27640  sltlin  27661  orngsqr  33282  weiunso  36454  fin2so  37601  fnwe2lem3  43041  prproropf1olem4  47507