Theorem sowlin 4048

Description: A strict order relation satisfies weak linearity. (Contributed by Jim Kingdon, 6-Oct-2018.)

Assertion

Ref	Expression
sowlin	⊢ ((𝑅 Or A ∧ (B ∈ A ∧ 𝐶 ∈ A ∧ 𝐷 ∈ A)) → (B𝑅𝐶 → (B𝑅𝐷 ∨ 𝐷𝑅𝐶)))

Proof of Theorem sowlin

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 3758	. . . . 5 ⊢ (x = B → (x𝑅y ↔ B𝑅y))
2		breq1 3758	. . . . . 6 ⊢ (x = B → (x𝑅z ↔ B𝑅z))
3	2	orbi1d 704	. . . . 5 ⊢ (x = B → ((x𝑅z ∨ z𝑅y) ↔ (B𝑅z ∨ z𝑅y)))
4	1, 3	imbi12d 223	. . . 4 ⊢ (x = B → ((x𝑅y → (x𝑅z ∨ z𝑅y)) ↔ (B𝑅y → (B𝑅z ∨ z𝑅y))))
5	4	imbi2d 219	. . 3 ⊢ (x = B → ((𝑅 Or A → (x𝑅y → (x𝑅z ∨ z𝑅y))) ↔ (𝑅 Or A → (B𝑅y → (B𝑅z ∨ z𝑅y)))))
6		breq2 3759	. . . . 5 ⊢ (y = 𝐶 → (B𝑅y ↔ B𝑅𝐶))
7		breq2 3759	. . . . . 6 ⊢ (y = 𝐶 → (z𝑅y ↔ z𝑅𝐶))
8	7	orbi2d 703	. . . . 5 ⊢ (y = 𝐶 → ((B𝑅z ∨ z𝑅y) ↔ (B𝑅z ∨ z𝑅𝐶)))
9	6, 8	imbi12d 223	. . . 4 ⊢ (y = 𝐶 → ((B𝑅y → (B𝑅z ∨ z𝑅y)) ↔ (B𝑅𝐶 → (B𝑅z ∨ z𝑅𝐶))))
10	9	imbi2d 219	. . 3 ⊢ (y = 𝐶 → ((𝑅 Or A → (B𝑅y → (B𝑅z ∨ z𝑅y))) ↔ (𝑅 Or A → (B𝑅𝐶 → (B𝑅z ∨ z𝑅𝐶)))))
11		breq2 3759	. . . . . 6 ⊢ (z = 𝐷 → (B𝑅z ↔ B𝑅𝐷))
12		breq1 3758	. . . . . 6 ⊢ (z = 𝐷 → (z𝑅𝐶 ↔ 𝐷𝑅𝐶))
13	11, 12	orbi12d 706	. . . . 5 ⊢ (z = 𝐷 → ((B𝑅z ∨ z𝑅𝐶) ↔ (B𝑅𝐷 ∨ 𝐷𝑅𝐶)))
14	13	imbi2d 219	. . . 4 ⊢ (z = 𝐷 → ((B𝑅𝐶 → (B𝑅z ∨ z𝑅𝐶)) ↔ (B𝑅𝐶 → (B𝑅𝐷 ∨ 𝐷𝑅𝐶))))
15	14	imbi2d 219	. . 3 ⊢ (z = 𝐷 → ((𝑅 Or A → (B𝑅𝐶 → (B𝑅z ∨ z𝑅𝐶))) ↔ (𝑅 Or A → (B𝑅𝐶 → (B𝑅𝐷 ∨ 𝐷𝑅𝐶)))))
16		df-iso 4025	. . . . 5 ⊢ (𝑅 Or A ↔ (𝑅 Po A ∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y))))
17		3anass 888	. . . . . . 7 ⊢ ((x ∈ A ∧ y ∈ A ∧ z ∈ A) ↔ (x ∈ A ∧ (y ∈ A ∧ z ∈ A)))
18		rsp 2363	. . . . . . . . 9 ⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y)) → (x ∈ A → ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y))))
19		rsp2 2365	. . . . . . . . 9 ⊢ (∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y)) → ((y ∈ A ∧ z ∈ A) → (x𝑅y → (x𝑅z ∨ z𝑅y))))
20	18, 19	syl6 29	. . . . . . . 8 ⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y)) → (x ∈ A → ((y ∈ A ∧ z ∈ A) → (x𝑅y → (x𝑅z ∨ z𝑅y)))))
21	20	impd 242	. . . . . . 7 ⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y)) → ((x ∈ A ∧ (y ∈ A ∧ z ∈ A)) → (x𝑅y → (x𝑅z ∨ z𝑅y))))
22	17, 21	syl5bi 141	. . . . . 6 ⊢ (∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y)) → ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (x𝑅y → (x𝑅z ∨ z𝑅y))))
23	22	adantl 262	. . . . 5 ⊢ ((𝑅 Po A ∧ ∀x ∈ A ∀y ∈ A ∀z ∈ A (x𝑅y → (x𝑅z ∨ z𝑅y))) → ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (x𝑅y → (x𝑅z ∨ z𝑅y))))
24	16, 23	sylbi 114	. . . 4 ⊢ (𝑅 Or A → ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (x𝑅y → (x𝑅z ∨ z𝑅y))))
25	24	com12 27	. . 3 ⊢ ((x ∈ A ∧ y ∈ A ∧ z ∈ A) → (𝑅 Or A → (x𝑅y → (x𝑅z ∨ z𝑅y))))
26	5, 10, 15, 25	vtocl3ga 2617	. 2 ⊢ ((B ∈ A ∧ 𝐶 ∈ A ∧ 𝐷 ∈ A) → (𝑅 Or A → (B𝑅𝐶 → (B𝑅𝐷 ∨ 𝐷𝑅𝐶))))
27	26	impcom 116	1 ⊢ ((𝑅 Or A ∧ (B ∈ A ∧ 𝐶 ∈ A ∧ 𝐷 ∈ A)) → (B𝑅𝐶 → (B𝑅𝐷 ∨ 𝐷𝑅𝐶)))

Syntax hints:   → wi 4   ∧ wa 97   ∨ wo 628   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ∀wral 2300   class class class wbr 3755   Po wpo 4022   Or wor 4023

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-v 2553  df-un 2916  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-iso 4025

This theorem is referenced by:  sotri2  4665  sotri3  4666  addextpr  6593  cauappcvgprlemloc  6624  caucvgprlemloc  6646  ltsosr  6692  axpre-ltwlin  6767  xrlelttr  8492  xrltletr  8493  xrletr  8494