Theorem solin 5567

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 5103	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥𝑅𝑦 ↔ 𝐵𝑅𝑦))
2		eqeq1 2741	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑥 = 𝑦 ↔ 𝐵 = 𝑦))
3		breq2 5104	. . . . 5 ⊢ (𝑥 = 𝐵 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝐵))
4	1, 2, 3	3orbi123d 1438	. . . 4 ⊢ (𝑥 = 𝐵 → ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝐵𝑅𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦𝑅𝐵)))
5	4	imbi2d 340	. . 3 ⊢ (𝑥 = 𝐵 → ((𝑅 Or 𝐴 → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦𝑅𝐵))))
6		breq2 5104	. . . . 5 ⊢ (𝑦 = 𝐶 → (𝐵𝑅𝑦 ↔ 𝐵𝑅𝐶))
7		eqeq2 2749	. . . . 5 ⊢ (𝑦 = 𝐶 → (𝐵 = 𝑦 ↔ 𝐵 = 𝐶))
8		breq1 5103	. . . . 5 ⊢ (𝑦 = 𝐶 → (𝑦𝑅𝐵 ↔ 𝐶𝑅𝐵))
9	6, 7, 8	3orbi123d 1438	. . . 4 ⊢ (𝑦 = 𝐶 → ((𝐵𝑅𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦𝑅𝐵) ↔ (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
10	9	imbi2d 340	. . 3 ⊢ (𝑦 = 𝐶 → ((𝑅 Or 𝐴 → (𝐵𝑅𝑦 ∨ 𝐵 = 𝑦 ∨ 𝑦𝑅𝐵)) ↔ (𝑅 Or 𝐴 → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))))
11		df-so 5541	. . . . 5 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
12		breq1 5103	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥𝑅𝑦 ↔ 𝑧𝑅𝑦))
13		equequ1 2027	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑧 = 𝑦))
14		breq2 5104	. . . . . . . . . 10 ⊢ (𝑥 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑦𝑅𝑧))
15	12, 13, 14	3orbi123d 1438	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑧𝑅𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦𝑅𝑧)))
16	15	ralbidv 3161	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑧𝑅𝑦 ∨ 𝑧 = 𝑦 ∨ 𝑦𝑅𝑧)))
17	16	rspw 3215	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
18		breq2 5104	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑥𝑅𝑦 ↔ 𝑥𝑅𝑧))
19		equequ2 2028	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧))
20		breq1 5103	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑥 ↔ 𝑧𝑅𝑥))
21	18, 19, 20	3orbi123d 1438	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → ((𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ (𝑥𝑅𝑧 ∨ 𝑥 = 𝑧 ∨ 𝑧𝑅𝑥)))
22	21	rspw 3215	. . . . . . 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 3535	. 2 ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝑅 Or 𝐴 → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)))
28	27	impcom 407	1 ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ∀wral 3052   class class class wbr 5100   Po wpo 5538   Or wor 5539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-so 5541

This theorem is referenced by:  sotric  5570  sotrieq  5571  somo  5579  wecmpep  5624  sorpssi  7684  soxp  8081  infsupprpr  9421  wemaplem2  9464  fpwwe2lem11  10564  fpwwe2lem12  10565  lttri4  11229  xmullem  13191  xmulasslem  13212  orngsqr  20811  noresle  27677  nosupbnd1lem6  27693  noinfbnd1lem6  27708  ltslin  27729  weiunso  36679  fin2so  37852  fnwe2lem3  43403  prproropf1olem4  47860