Theorem ltsopr 7590

Description: Positive real 'less than' is a weak linear order (in the sense of df-iso 4295). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)

Assertion

Ref	Expression
ltsopr	⊢ <P Or P

Proof of Theorem ltsopr

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

Step	Hyp	Ref	Expression
1		ltpopr 7589	. 2 ⊢ <P Po P
2		ltdfpr 7500	. . . . 5 ⊢ ((𝑥 ∈ P ∧ 𝑦 ∈ P) → (𝑥<P 𝑦 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))))
3	2	3adant3 1017	. . . 4 ⊢ ((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) → (𝑥<P 𝑦 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))))
4		prop 7469	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ P → ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ P)
5		prnminu 7483	. . . . . . . . . . . 12 ⊢ ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ P ∧ 𝑞 ∈ (2nd ‘𝑥)) → ∃𝑟 ∈ (2nd ‘𝑥)𝑟 <Q 𝑞)
6	4, 5	sylan 283	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ P ∧ 𝑞 ∈ (2nd ‘𝑥)) → ∃𝑟 ∈ (2nd ‘𝑥)𝑟 <Q 𝑞)
7		prop 7469	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ P → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ P)
8		prnmaxl 7482	. . . . . . . . . . . 12 ⊢ ((⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ P ∧ 𝑞 ∈ (1st ‘𝑦)) → ∃𝑠 ∈ (1st ‘𝑦)𝑞 <Q 𝑠)
9	7, 8	sylan 283	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ P ∧ 𝑞 ∈ (1st ‘𝑦)) → ∃𝑠 ∈ (1st ‘𝑦)𝑞 <Q 𝑠)
10	6, 9	anim12i 338	. . . . . . . . . 10 ⊢ (((𝑥 ∈ P ∧ 𝑞 ∈ (2nd ‘𝑥)) ∧ (𝑦 ∈ P ∧ 𝑞 ∈ (1st ‘𝑦))) → (∃𝑟 ∈ (2nd ‘𝑥)𝑟 <Q 𝑞 ∧ ∃𝑠 ∈ (1st ‘𝑦)𝑞 <Q 𝑠))
11	10	an4s 588	. . . . . . . . 9 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) → (∃𝑟 ∈ (2nd ‘𝑥)𝑟 <Q 𝑞 ∧ ∃𝑠 ∈ (1st ‘𝑦)𝑞 <Q 𝑠))
12		reeanv 2646	. . . . . . . . 9 ⊢ (∃𝑟 ∈ (2nd ‘𝑥)∃𝑠 ∈ (1st ‘𝑦)(𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠) ↔ (∃𝑟 ∈ (2nd ‘𝑥)𝑟 <Q 𝑞 ∧ ∃𝑠 ∈ (1st ‘𝑦)𝑞 <Q 𝑠))
13	11, 12	sylibr 134	. . . . . . . 8 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) → ∃𝑟 ∈ (2nd ‘𝑥)∃𝑠 ∈ (1st ‘𝑦)(𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠))
14	13	3adantl3 1155	. . . . . . 7 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) → ∃𝑟 ∈ (2nd ‘𝑥)∃𝑠 ∈ (1st ‘𝑦)(𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠))
15		ltsonq 7392	. . . . . . . . . . . . 13 ⊢ <Q Or Q
16		ltrelnq 7359	. . . . . . . . . . . . 13 ⊢ <Q ⊆ (Q × Q)
17	15, 16	sotri 5021	. . . . . . . . . . . 12 ⊢ ((𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠) → 𝑟 <Q 𝑠)
18	17	adantl 277	. . . . . . . . . . 11 ⊢ (((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦))) ∧ (𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠)) → 𝑟 <Q 𝑠)
19		prop 7469	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ P → ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ ∈ P)
20		prloc 7485	. . . . . . . . . . . . . . . 16 ⊢ ((⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ ∈ P ∧ 𝑟 <Q 𝑠) → (𝑟 ∈ (1st ‘𝑧) ∨ 𝑠 ∈ (2nd ‘𝑧)))
21	19, 20	sylan 283	. . . . . . . . . . . . . . 15 ⊢ ((𝑧 ∈ P ∧ 𝑟 <Q 𝑠) → (𝑟 ∈ (1st ‘𝑧) ∨ 𝑠 ∈ (2nd ‘𝑧)))
22	21	3ad2antl3 1161	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑟 <Q 𝑠) → (𝑟 ∈ (1st ‘𝑧) ∨ 𝑠 ∈ (2nd ‘𝑧)))
23	22	ex 115	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) → (𝑟 <Q 𝑠 → (𝑟 ∈ (1st ‘𝑧) ∨ 𝑠 ∈ (2nd ‘𝑧))))
24	23	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) → (𝑟 <Q 𝑠 → (𝑟 ∈ (1st ‘𝑧) ∨ 𝑠 ∈ (2nd ‘𝑧))))
25	24	ad2antrr 488	. . . . . . . . . . 11 ⊢ (((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦))) ∧ (𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠)) → (𝑟 <Q 𝑠 → (𝑟 ∈ (1st ‘𝑧) ∨ 𝑠 ∈ (2nd ‘𝑧))))
26	18, 25	mpd 13	. . . . . . . . . 10 ⊢ (((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦))) ∧ (𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠)) → (𝑟 ∈ (1st ‘𝑧) ∨ 𝑠 ∈ (2nd ‘𝑧)))
27		elprnqu 7476	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ P ∧ 𝑟 ∈ (2nd ‘𝑥)) → 𝑟 ∈ Q)
28	4, 27	sylan 283	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ P ∧ 𝑟 ∈ (2nd ‘𝑥)) → 𝑟 ∈ Q)
29		ax-ia3 108	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑟 ∈ (2nd ‘𝑥) → (𝑟 ∈ (1st ‘𝑧) → (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧))))
30	29	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 ∈ P ∧ 𝑟 ∈ (2nd ‘𝑥)) → (𝑟 ∈ (1st ‘𝑧) → (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧))))
31		19.8a 1590	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑟 ∈ Q ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧))) → ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧))))
32	28, 30, 31	syl6an 1434	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ P ∧ 𝑟 ∈ (2nd ‘𝑥)) → (𝑟 ∈ (1st ‘𝑧) → ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧)))))
33	32	3ad2antl1 1159	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑟 ∈ (2nd ‘𝑥)) → (𝑟 ∈ (1st ‘𝑧) → ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧)))))
34	33	imp 124	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑟 ∈ (2nd ‘𝑥)) ∧ 𝑟 ∈ (1st ‘𝑧)) → ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧))))
35		df-rex 2461	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧)) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧))))
36	34, 35	sylibr 134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑟 ∈ (2nd ‘𝑥)) ∧ 𝑟 ∈ (1st ‘𝑧)) → ∃𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧)))
37		ltdfpr 7500	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ P ∧ 𝑧 ∈ P) → (𝑥<P 𝑧 ↔ ∃𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧))))
38	37	biimprd 158	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ P ∧ 𝑧 ∈ P) → (∃𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧)) → 𝑥<P 𝑧))
39	38	3adant2 1016	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) → (∃𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧)) → 𝑥<P 𝑧))
40	39	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑟 ∈ (2nd ‘𝑥)) ∧ 𝑟 ∈ (1st ‘𝑧)) → (∃𝑟 ∈ Q (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑟 ∈ (1st ‘𝑧)) → 𝑥<P 𝑧))
41	36, 40	mpd 13	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑟 ∈ (2nd ‘𝑥)) ∧ 𝑟 ∈ (1st ‘𝑧)) → 𝑥<P 𝑧)
42	41	ex 115	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑟 ∈ (2nd ‘𝑥)) → (𝑟 ∈ (1st ‘𝑧) → 𝑥<P 𝑧))
43	42	adantrr 479	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦))) → (𝑟 ∈ (1st ‘𝑧) → 𝑥<P 𝑧))
44		elprnql 7475	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ P ∧ 𝑠 ∈ (1st ‘𝑦)) → 𝑠 ∈ Q)
45	7, 44	sylan 283	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ P ∧ 𝑠 ∈ (1st ‘𝑦)) → 𝑠 ∈ Q)
46		pm3.21 264	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑠 ∈ (1st ‘𝑦) → (𝑠 ∈ (2nd ‘𝑧) → (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦))))
47	46	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ P ∧ 𝑠 ∈ (1st ‘𝑦)) → (𝑠 ∈ (2nd ‘𝑧) → (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦))))
48		19.8a 1590	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑠 ∈ Q ∧ (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦))) → ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦))))
49	45, 47, 48	syl6an 1434	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ P ∧ 𝑠 ∈ (1st ‘𝑦)) → (𝑠 ∈ (2nd ‘𝑧) → ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦)))))
50	49	3ad2antl2 1160	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑠 ∈ (1st ‘𝑦)) → (𝑠 ∈ (2nd ‘𝑧) → ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦)))))
51	50	imp 124	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑠 ∈ (1st ‘𝑦)) ∧ 𝑠 ∈ (2nd ‘𝑧)) → ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦))))
52		df-rex 2461	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑠 ∈ Q (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦)) ↔ ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦))))
53	51, 52	sylibr 134	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑠 ∈ (1st ‘𝑦)) ∧ 𝑠 ∈ (2nd ‘𝑧)) → ∃𝑠 ∈ Q (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦)))
54		ltdfpr 7500	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ P ∧ 𝑦 ∈ P) → (𝑧<P 𝑦 ↔ ∃𝑠 ∈ Q (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦))))
55	54	biimprd 158	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ P ∧ 𝑦 ∈ P) → (∃𝑠 ∈ Q (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦)) → 𝑧<P 𝑦))
56	55	ancoms 268	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ P ∧ 𝑧 ∈ P) → (∃𝑠 ∈ Q (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦)) → 𝑧<P 𝑦))
57	56	3adant1 1015	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) → (∃𝑠 ∈ Q (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦)) → 𝑧<P 𝑦))
58	57	ad2antrr 488	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑠 ∈ (1st ‘𝑦)) ∧ 𝑠 ∈ (2nd ‘𝑧)) → (∃𝑠 ∈ Q (𝑠 ∈ (2nd ‘𝑧) ∧ 𝑠 ∈ (1st ‘𝑦)) → 𝑧<P 𝑦))
59	53, 58	mpd 13	. . . . . . . . . . . . . . 15 ⊢ ((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑠 ∈ (1st ‘𝑦)) ∧ 𝑠 ∈ (2nd ‘𝑧)) → 𝑧<P 𝑦)
60	59	ex 115	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ 𝑠 ∈ (1st ‘𝑦)) → (𝑠 ∈ (2nd ‘𝑧) → 𝑧<P 𝑦))
61	60	adantrl 478	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦))) → (𝑠 ∈ (2nd ‘𝑧) → 𝑧<P 𝑦))
62	43, 61	orim12d 786	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦))) → ((𝑟 ∈ (1st ‘𝑧) ∨ 𝑠 ∈ (2nd ‘𝑧)) → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦)))
63	62	adantlr 477	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦))) → ((𝑟 ∈ (1st ‘𝑧) ∨ 𝑠 ∈ (2nd ‘𝑧)) → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦)))
64	63	adantr 276	. . . . . . . . . 10 ⊢ (((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦))) ∧ (𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠)) → ((𝑟 ∈ (1st ‘𝑧) ∨ 𝑠 ∈ (2nd ‘𝑧)) → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦)))
65	26, 64	mpd 13	. . . . . . . . 9 ⊢ (((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦))) ∧ (𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠)) → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦))
66	65	ex 115	. . . . . . . 8 ⊢ ((((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) ∧ (𝑟 ∈ (2nd ‘𝑥) ∧ 𝑠 ∈ (1st ‘𝑦))) → ((𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠) → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦)))
67	66	rexlimdvva 2602	. . . . . . 7 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) → (∃𝑟 ∈ (2nd ‘𝑥)∃𝑠 ∈ (1st ‘𝑦)(𝑟 <Q 𝑞 ∧ 𝑞 <Q 𝑠) → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦)))
68	14, 67	mpd 13	. . . . . 6 ⊢ (((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) ∧ (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦))) → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦))
69	68	ex 115	. . . . 5 ⊢ ((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) → ((𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)) → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦)))
70	69	rexlimdvw 2598	. . . 4 ⊢ ((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) → (∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑥) ∧ 𝑞 ∈ (1st ‘𝑦)) → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦)))
71	3, 70	sylbid 150	. . 3 ⊢ ((𝑥 ∈ P ∧ 𝑦 ∈ P ∧ 𝑧 ∈ P) → (𝑥<P 𝑦 → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦)))
72	71	rgen3 2564	. 2 ⊢ ∀𝑥 ∈ P ∀𝑦 ∈ P ∀𝑧 ∈ P (𝑥<P 𝑦 → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦))
73		df-iso 4295	. 2 ⊢ (<P Or P ↔ (<P Po P ∧ ∀𝑥 ∈ P ∀𝑦 ∈ P ∀𝑧 ∈ P (𝑥<P 𝑦 → (𝑥<P 𝑧 ∨ 𝑧<P 𝑦))))
74	1, 72, 73	mpbir2an 942	1 ⊢ <P Or P

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708   ∧ w3a 978  ∃wex 1492   ∈ wcel 2148  ∀wral 2455  ∃wrex 2456  ⟨cop 3595   class class class wbr 4001   Po wpo 4292   Or wor 4293  ‘cfv 5213  1^st c1st 6134  2^nd c2nd 6135  Qcnq 7274   <_Q cltq 7279  Pcnp 7285  <_P cltp 7289

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4116  ax-sep 4119  ax-nul 4127  ax-pow 4172  ax-pr 4207  ax-un 4431  ax-setind 4534  ax-iinf 4585

This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-int 3844  df-iun 3887  df-br 4002  df-opab 4063  df-mpt 4064  df-tr 4100  df-eprel 4287  df-id 4291  df-po 4294  df-iso 4295  df-iord 4364  df-on 4366  df-suc 4369  df-iom 4588  df-xp 4630  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-rn 4635  df-res 4636  df-ima 4637  df-iota 5175  df-fun 5215  df-fn 5216  df-f 5217  df-f1 5218  df-fo 5219  df-f1o 5220  df-fv 5221  df-ov 5873  df-oprab 5874  df-mpo 5875  df-1st 6136  df-2nd 6137  df-recs 6301  df-irdg 6366  df-oadd 6416  df-omul 6417  df-er 6530  df-ec 6532  df-qs 6536  df-ni 7298  df-mi 7300  df-lti 7301  df-enq 7341  df-nqqs 7342  df-ltnqqs 7347  df-inp 7460  df-iltp 7464

This theorem is referenced by:  prplnqu  7614  addextpr  7615  caucvgprprlemk  7677  caucvgprprlemnkltj  7683  caucvgprprlemnkeqj  7684  caucvgprprlemnjltk  7685  caucvgprprlemnbj  7687  caucvgprprlemml  7688  caucvgprprlemlol  7692  caucvgprprlemupu  7694  caucvgprprlemloc  7697  caucvgprprlemaddq  7702  suplocexprlemmu  7712  lttrsr  7756  ltposr  7757  ltsosr  7758  archsr  7776