Theorem ltsosr 3997

Description: Signed real 'less than' is a strict ordering.

Assertion

Ref	Expression
ltsosr	⊢ <R Or R

Proof of Theorem ltsosr

Step	Hyp	Ref	Expression
1		df-nr 3961	. . 3 ⊢ R = ((P × P) / ~R )
2		breq1 2065	. . . . 5 ⊢ ([⟨x, y⟩] ~R = f → ([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ↔ f <R [⟨z, w⟩] ~R ))
3		cleq1 1107	. . . . . . 7 ⊢ ([⟨x, y⟩] ~R = f → ([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ↔ f = [⟨z, w⟩] ~R ))
4		breq2 2066	. . . . . . 7 ⊢ ([⟨x, y⟩] ~R = f → ([⟨z, w⟩] ~R <R [⟨x, y⟩] ~R ↔ [⟨z, w⟩] ~R <R f))
5	3, 4	orbi12d 475	. . . . . 6 ⊢ ([⟨x, y⟩] ~R = f → (([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R [⟨x, y⟩] ~R ) ↔ (f = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R f)))
6	5	negbid 463	. . . . 5 ⊢ ([⟨x, y⟩] ~R = f → (¬ ([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R [⟨x, y⟩] ~R ) ↔ ¬ (f = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R f)))
7	2, 6	bibi12d 477	. . . 4 ⊢ ([⟨x, y⟩] ~R = f → (([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ↔ ¬ ([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R [⟨x, y⟩] ~R )) ↔ (f <R [⟨z, w⟩] ~R ↔ ¬ (f = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R f))))
8	2	anbi1d 469	. . . . 5 ⊢ ([⟨x, y⟩] ~R = f → (([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) ↔ (f <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R )))
9		breq1 2065	. . . . 5 ⊢ ([⟨x, y⟩] ~R = f → ([⟨x, y⟩] ~R <R [⟨v, u⟩] ~R ↔ f <R [⟨v, u⟩] ~R ))
10	8, 9	imbi12d 474	. . . 4 ⊢ ([⟨x, y⟩] ~R = f → ((([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → [⟨x, y⟩] ~R <R [⟨v, u⟩] ~R ) ↔ ((f <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → f <R [⟨v, u⟩] ~R )))
11	7, 10	anbi12d 476	. . 3 ⊢ ([⟨x, y⟩] ~R = f → ((([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ↔ ¬ ([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R [⟨x, y⟩] ~R )) ∧ (([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → [⟨x, y⟩] ~R <R [⟨v, u⟩] ~R )) ↔ ((f <R [⟨z, w⟩] ~R ↔ ¬ (f = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R f)) ∧ ((f <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → f <R [⟨v, u⟩] ~R ))))
12		breq2 2066	. . . . 5 ⊢ ([⟨z, w⟩] ~R = g → (f <R [⟨z, w⟩] ~R ↔ f <R g))
13		cleq2 1110	. . . . . . 7 ⊢ ([⟨z, w⟩] ~R = g → (f = [⟨z, w⟩] ~R ↔ f = g))
14		breq1 2065	. . . . . . 7 ⊢ ([⟨z, w⟩] ~R = g → ([⟨z, w⟩] ~R <R f ↔ g <R f))
15	13, 14	orbi12d 475	. . . . . 6 ⊢ ([⟨z, w⟩] ~R = g → ((f = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R f) ↔ (f = g ∨ g <R f)))
16	15	negbid 463	. . . . 5 ⊢ ([⟨z, w⟩] ~R = g → (¬ (f = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R f) ↔ ¬ (f = g ∨ g <R f)))
17	12, 16	bibi12d 477	. . . 4 ⊢ ([⟨z, w⟩] ~R = g → ((f <R [⟨z, w⟩] ~R ↔ ¬ (f = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R f)) ↔ (f <R g ↔ ¬ (f = g ∨ g <R f))))
18		breq1 2065	. . . . . 6 ⊢ ([⟨z, w⟩] ~R = g → ([⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ↔ g <R [⟨v, u⟩] ~R ))
19	12, 18	anbi12d 476	. . . . 5 ⊢ ([⟨z, w⟩] ~R = g → ((f <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) ↔ (f <R g ∧ g <R [⟨v, u⟩] ~R )))
20	19	imbi1d 465	. . . 4 ⊢ ([⟨z, w⟩] ~R = g → (((f <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → f <R [⟨v, u⟩] ~R ) ↔ ((f <R g ∧ g <R [⟨v, u⟩] ~R ) → f <R [⟨v, u⟩] ~R )))
21	17, 20	anbi12d 476	. . 3 ⊢ ([⟨z, w⟩] ~R = g → (((f <R [⟨z, w⟩] ~R ↔ ¬ (f = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R f)) ∧ ((f <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → f <R [⟨v, u⟩] ~R )) ↔ ((f <R g ↔ ¬ (f = g ∨ g <R f)) ∧ ((f <R g ∧ g <R [⟨v, u⟩] ~R ) → f <R [⟨v, u⟩] ~R ))))
22		breq2 2066	. . . . . 6 ⊢ ([⟨v, u⟩] ~R = h → (g <R [⟨v, u⟩] ~R ↔ g <R h))
23	22	anbi2d 468	. . . . 5 ⊢ ([⟨v, u⟩] ~R = h → ((f <R g ∧ g <R [⟨v, u⟩] ~R ) ↔ (f <R g ∧ g <R h)))
24		breq2 2066	. . . . 5 ⊢ ([⟨v, u⟩] ~R = h → (f <R [⟨v, u⟩] ~R ↔ f <R h))
25	23, 24	imbi12d 474	. . . 4 ⊢ ([⟨v, u⟩] ~R = h → (((f <R g ∧ g <R [⟨v, u⟩] ~R ) → f <R [⟨v, u⟩] ~R ) ↔ ((f <R g ∧ g <R h) → f <R h)))
26	25	anbi2d 468	. . 3 ⊢ ([⟨v, u⟩] ~R = h → (((f <R g ↔ ¬ (f = g ∨ g <R f)) ∧ ((f <R g ∧ g <R [⟨v, u⟩] ~R ) → f <R [⟨v, u⟩] ~R )) ↔ ((f <R g ↔ ¬ (f = g ∨ g <R f)) ∧ ((f <R g ∧ g <R h) → f <R h))))
27		ltsopr 3930	. . . . . . . . . 10 ⊢ <P Or P
28		sotric 2148	. . . . . . . . . 10 ⊢ ((<P Or P ∧ ((x +P w) ∈ P ∧ (y +P z) ∈ P)) → ((x +P w)<P (y +P z) ↔ ¬ ((x +P w) = (y +P z) ∨ (y +P z)<P (x +P w))))
29	27, 28	mpan 518	. . . . . . . . 9 ⊢ (((x +P w) ∈ P ∧ (y +P z) ∈ P) → ((x +P w)<P (y +P z) ↔ ¬ ((x +P w) = (y +P z) ∨ (y +P z)<P (x +P w))))
30		addclpr 3914	. . . . . . . . 9 ⊢ ((x ∈ P ∧ w ∈ P) → (x +P w) ∈ P)
31		addclpr 3914	. . . . . . . . 9 ⊢ ((y ∈ P ∧ z ∈ P) → (y +P z) ∈ P)
32	29, 30, 31	syl2an 349	. . . . . . . 8 ⊢ (((x ∈ P ∧ w ∈ P) ∧ (y ∈ P ∧ z ∈ P)) → ((x +P w)<P (y +P z) ↔ ¬ ((x +P w) = (y +P z) ∨ (y +P z)<P (x +P w))))
33	32	an42s 391	. . . . . . 7 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ((x +P w)<P (y +P z) ↔ ¬ ((x +P w) = (y +P z) ∨ (y +P z)<P (x +P w))))
34		enreceq 3971	. . . . . . . . 9 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ↔ (x +P w) = (y +P z)))
35		visset 1350	. . . . . . . . . . . 12 ⊢ z ∈ V
36		visset 1350	. . . . . . . . . . . 12 ⊢ w ∈ V
37		visset 1350	. . . . . . . . . . . 12 ⊢ x ∈ V
38		visset 1350	. . . . . . . . . . . 12 ⊢ y ∈ V
39	35, 36, 37, 38	ltsrpr 3980	. . . . . . . . . . 11 ⊢ ([⟨z, w⟩] ~R <R [⟨x, y⟩] ~R ↔ (z +P y)<P (w +P x))
40	35, 38	addcompr 3917	. . . . . . . . . . . 12 ⊢ (z +P y) = (y +P z)
41	36, 37	addcompr 3917	. . . . . . . . . . . 12 ⊢ (w +P x) = (x +P w)
42	40, 41	breq12i 2070	. . . . . . . . . . 11 ⊢ ((z +P y)<P (w +P x) ↔ (y +P z)<P (x +P w))
43	39, 42	bitr 151	. . . . . . . . . 10 ⊢ ([⟨z, w⟩] ~R <R [⟨x, y⟩] ~R ↔ (y +P z)<P (x +P w))
44	43	a1i 7	. . . . . . . . 9 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ([⟨z, w⟩] ~R <R [⟨x, y⟩] ~R ↔ (y +P z)<P (x +P w)))
45	34, 44	orbi12d 475	. . . . . . . 8 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → (([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R [⟨x, y⟩] ~R ) ↔ ((x +P w) = (y +P z) ∨ (y +P z)<P (x +P w))))
46	45	negbid 463	. . . . . . 7 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → (¬ ([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R [⟨x, y⟩] ~R ) ↔ ¬ ((x +P w) = (y +P z) ∨ (y +P z)<P (x +P w))))
47	33, 46	bitr4d 409	. . . . . 6 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ((x +P w)<P (y +P z) ↔ ¬ ([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R [⟨x, y⟩] ~R )))
48	37, 38, 35, 36	ltsrpr 3980	. . . . . 6 ⊢ ([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ↔ (x +P w)<P (y +P z))
49	47, 48	syl5bb 410	. . . . 5 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P)) → ([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ↔ ¬ ([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R [⟨x, y⟩] ~R )))
50	49	3adant3 599	. . . 4 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → ([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ↔ ¬ ([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R [⟨x, y⟩] ~R )))
51		oprex 3018	. . . . . . . . . . . 12 ⊢ (x +P w) ∈ V
52		oprex 3018	. . . . . . . . . . . 12 ⊢ (y +P z) ∈ V
53		visset 1350	. . . . . . . . . . . . 13 ⊢ f ∈ V
54		visset 1350	. . . . . . . . . . . . 13 ⊢ g ∈ V
55	53, 54	ltapr 3945	. . . . . . . . . . . 12 ⊢ (h ∈ P → (f<P g ↔ (h +P f)<P (h +P g)))
56		visset 1350	. . . . . . . . . . . 12 ⊢ u ∈ V
57	53, 54	addcompr 3917	. . . . . . . . . . . 12 ⊢ (f +P g) = (g +P f)
58	51, 52, 55, 56, 57	caoprord2 3071	. . . . . . . . . . 11 ⊢ (u ∈ P → ((x +P w)<P (y +P z) ↔ ((x +P w) +P u)<P ((y +P z) +P u)))
59	36, 56	addasspr 3918	. . . . . . . . . . . 12 ⊢ ((x +P w) +P u) = (x +P (w +P u))
60	35, 56	addasspr 3918	. . . . . . . . . . . 12 ⊢ ((y +P z) +P u) = (y +P (z +P u))
61	59, 60	breq12i 2070	. . . . . . . . . . 11 ⊢ (((x +P w) +P u)<P ((y +P z) +P u) ↔ (x +P (w +P u))<P (y +P (z +P u)))
62	58, 61	syl6bb 414	. . . . . . . . . 10 ⊢ (u ∈ P → ((x +P w)<P (y +P z) ↔ (x +P (w +P u))<P (y +P (z +P u))))
63	62, 48	syl5bb 410	. . . . . . . . 9 ⊢ (u ∈ P → ([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ↔ (x +P (w +P u))<P (y +P (z +P u))))
64		oprex 3018	. . . . . . . . . . 11 ⊢ (z +P u) ∈ V
65		oprex 3018	. . . . . . . . . . 11 ⊢ (w +P v) ∈ V
66	64, 65	ltapr 3945	. . . . . . . . . 10 ⊢ (y ∈ P → ((z +P u)<P (w +P v) ↔ (y +P (z +P u))<P (y +P (w +P v))))
67		visset 1350	. . . . . . . . . . 11 ⊢ v ∈ V
68	35, 36, 67, 56	ltsrpr 3980	. . . . . . . . . 10 ⊢ ([⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ↔ (z +P u)<P (w +P v))
69	66, 68	syl5bb 410	. . . . . . . . 9 ⊢ (y ∈ P → ([⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ↔ (y +P (z +P u))<P (y +P (w +P v))))
70	63, 69	bi2anan9r 479	. . . . . . . 8 ⊢ ((y ∈ P ∧ u ∈ P) → (([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) ↔ ((x +P (w +P u))<P (y +P (z +P u)) ∧ (y +P (z +P u))<P (y +P (w +P v)))))
71		oprex 3018	. . . . . . . . . 10 ⊢ (x +P (w +P u)) ∈ V
72		ltrelpr 3895	. . . . . . . . . 10 ⊢ <P ⊆ (P × P)
73		oprex 3018	. . . . . . . . . 10 ⊢ (y +P (z +P u)) ∈ V
74		oprex 3018	. . . . . . . . . 10 ⊢ (y +P (w +P v)) ∈ V
75	71, 27, 72, 73, 74	sotri 2630	. . . . . . . . 9 ⊢ (((x +P (w +P u))<P (y +P (z +P u)) ∧ (y +P (z +P u))<P (y +P (w +P v))) → (x +P (w +P u))<P (y +P (w +P v)))
76		oprex 3018	. . . . . . . . . . 11 ⊢ (x +P u) ∈ V
77		dmplp 3909	. . . . . . . . . . 11 ⊢ dom +P = (P × P)
78		0npr 3890	. . . . . . . . . . 11 ⊢ ¬ ∅ ∈ P
79		oprex 3018	. . . . . . . . . . . 12 ⊢ (y +P v) ∈ V
80	76, 79	ltapr 3945	. . . . . . . . . . 11 ⊢ (w ∈ P → ((x +P u)<P (y +P v) ↔ (w +P (x +P u))<P (w +P (y +P v))))
81	76, 77, 72, 78, 80	ndmordi 3065	. . . . . . . . . 10 ⊢ ((w +P (x +P u))<P (w +P (y +P v)) → (x +P u)<P (y +P v))
82		visset 1350	. . . . . . . . . . . . 13 ⊢ h ∈ V
83	54, 82	addasspr 3918	. . . . . . . . . . . 12 ⊢ ((f +P g) +P h) = (f +P (g +P h))
84	37, 36, 56, 57, 83	caopr12 3075	. . . . . . . . . . 11 ⊢ (x +P (w +P u)) = (w +P (x +P u))
85	38, 36, 67, 57, 83	caopr12 3075	. . . . . . . . . . 11 ⊢ (y +P (w +P v)) = (w +P (y +P v))
86	84, 85	breq12i 2070	. . . . . . . . . 10 ⊢ ((x +P (w +P u))<P (y +P (w +P v)) ↔ (w +P (x +P u))<P (w +P (y +P v)))
87	37, 38, 67, 56	ltsrpr 3980	. . . . . . . . . 10 ⊢ ([⟨x, y⟩] ~R <R [⟨v, u⟩] ~R ↔ (x +P u)<P (y +P v))
88	81, 86, 87	3imtr4 192	. . . . . . . . 9 ⊢ ((x +P (w +P u))<P (y +P (w +P v)) → [⟨x, y⟩] ~R <R [⟨v, u⟩] ~R )
89	75, 88	syl 12	. . . . . . . 8 ⊢ (((x +P (w +P u))<P (y +P (z +P u)) ∧ (y +P (z +P u))<P (y +P (w +P v))) → [⟨x, y⟩] ~R <R [⟨v, u⟩] ~R )
90	70, 89	syl6bi 187	. . . . . . 7 ⊢ ((y ∈ P ∧ u ∈ P) → (([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → [⟨x, y⟩] ~R <R [⟨v, u⟩] ~R ))
91	90	adantrl 311	. . . . . 6 ⊢ ((y ∈ P ∧ (v ∈ P ∧ u ∈ P)) → (([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → [⟨x, y⟩] ~R <R [⟨v, u⟩] ~R ))
92	91	adantll 309	. . . . 5 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → [⟨x, y⟩] ~R <R [⟨v, u⟩] ~R ))
93	92	3adant2 598	. . . 4 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → [⟨x, y⟩] ~R <R [⟨v, u⟩] ~R ))
94	50, 93	jca 236	. . 3 ⊢ (((x ∈ P ∧ y ∈ P) ∧ (z ∈ P ∧ w ∈ P) ∧ (v ∈ P ∧ u ∈ P)) → (([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ↔ ¬ ([⟨x, y⟩] ~R = [⟨z, w⟩] ~R ∨ [⟨z, w⟩] ~R <R [⟨x, y⟩] ~R )) ∧ (([⟨x, y⟩] ~R <R [⟨z, w⟩] ~R ∧ [⟨z, w⟩] ~R <R [⟨v, u⟩] ~R ) → [⟨x, y⟩] ~R <R [⟨v, u⟩] ~R )))
95	1, 11, 21, 26, 94	3ecoptocl 3241	. 2 ⊢ ((f ∈ R ∧ g ∈ R ∧ h ∈ R) → ((f <R g ↔ ¬ (f = g ∨ g <R f)) ∧ ((f <R g ∧ g <R h) → f <R h)))
96	95	so 2152	1 ⊢ <R Or R

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196   ∧ w3a 581   = weq 797   = wceq 1091   ∈ wcel 1092  ⟨cop 1810   class class class wbr 2054   Or wor 2059  (class class class)co 3001  [cec 3198  Pcnp 3779   +_P cpp 3781  <_P cltp 3783   ~_R cer 3786  Rcnr 3787   <_R cltr 3793

This theorem is referenced by:  1ne0sr 3999  addgt0sr 4007  sqgt0sr 4009  suppsr2 4017  suppsr3 4018  ltsor 4055

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-reu 1207  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-int 1966  df-iun 1996  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438  df-rdg 2970  df-opr 3003  df-oprab 3004  df-1o 3104  df-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-pli 3795  df-mi 3796  df-lti 3797  df-plpq 3829  df-mpq 3830  df-enq 3831  df-nq 3832  df-plq 3833  df-mq 3834  df-rq 3835  df-ltq 3836  df-1q 3837  df-np 3880  df-plp 3882  df-ltp 3884  df-enr 3960  df-nr 3961  df-ltr 3964

metamath.org