Theorem 3oalem2 5553

Description: Lemma for 3OA (weak) orthoarguesian law.

Hypotheses

Ref	Expression
3oalem1.1	⊢ B ∈ Cℋ
3oalem1.2	⊢ C ∈ Cℋ
3oalem1.3	⊢ R ∈ Cℋ
3oalem1.4	⊢ S ∈ Cℋ

Assertion

Ref	Expression
3oalem2	⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → v ∈ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))))

Distinct variable group(s):   x,y,z,w,v,B   x,C,y,z,w,v   x,R,y,z,w,v   x,S,y,z,w,v

Proof of Theorem 3oalem2

Step	Hyp	Ref	Expression
1		3oalem1.1	. . . . 5 ⊢ B ∈ Cℋ
2	1	chshi 5132	. . . 4 ⊢ B ∈ Sℋ
3		3oalem1.3	. . . . . 6 ⊢ R ∈ Cℋ
4	3	chshi 5132	. . . . 5 ⊢ R ∈ Sℋ
5		3oalem1.4	. . . . . . 7 ⊢ S ∈ Cℋ
6	5	chshi 5132	. . . . . 6 ⊢ S ∈ Sℋ
7		3oalem1.2	. . . . . . . . 9 ⊢ C ∈ Cℋ
8	7	chshi 5132	. . . . . . . 8 ⊢ C ∈ Sℋ
9	2, 8	shscl 5282	. . . . . . 7 ⊢ (B +ℋ C) ∈ Sℋ
10	4, 6	shscl 5282	. . . . . . 7 ⊢ (R +ℋ S) ∈ Sℋ
11	9, 10	shincl 5332	. . . . . 6 ⊢ ((B +ℋ C) ∩ (R +ℋ S)) ∈ Sℋ
12	6, 11	shscl 5282	. . . . 5 ⊢ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))) ∈ Sℋ
13	4, 12	shincl 5332	. . . 4 ⊢ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S)))) ∈ Sℋ
14	2, 13	shsva 5334	. . 3 ⊢ ((x ∈ B ∧ y ∈ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))) → (x +v y) ∈ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))))
15		pm3.26 256	. . . 4 ⊢ ((x ∈ B ∧ y ∈ R) → x ∈ B)
16	15	ad2antll 320	. . 3 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → x ∈ B)
17		pm3.27 260	. . . . . 6 ⊢ ((x ∈ B ∧ y ∈ R) → y ∈ R)
18	17	ad2antll 320	. . . . 5 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → y ∈ R)
19	1, 7, 3, 5	3oalem1 5552	. . . . . . 7 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ v ∈ ℋ ) ∧ (z ∈ ℋ ∧ w ∈ ℋ )))
20		hvaddsub12t 5015	. . . . . . . . . . . . 13 ⊢ ((y ∈ ℋ ∧ w ∈ ℋ ∧ w ∈ ℋ ) → (y +v (w −v w)) = (w +v (y −v w)))
21	20	3expb 613	. . . . . . . . . . . 12 ⊢ ((y ∈ ℋ ∧ (w ∈ ℋ ∧ w ∈ ℋ )) → (y +v (w −v w)) = (w +v (y −v w)))
22	21	anabsan2 387	. . . . . . . . . . 11 ⊢ ((y ∈ ℋ ∧ w ∈ ℋ ) → (y +v (w −v w)) = (w +v (y −v w)))
23		hvsubidt 5005	. . . . . . . . . . . . 13 ⊢ (w ∈ ℋ → (w −v w) = 0v)
24	23	opreq2d 3013	. . . . . . . . . . . 12 ⊢ (w ∈ ℋ → (y +v (w −v w)) = (y +v 0v))
25		ax-hvaddid 4988	. . . . . . . . . . . 12 ⊢ (y ∈ ℋ → (y +v 0v) = y)
26	24, 25	sylan9eqr 1145	. . . . . . . . . . 11 ⊢ ((y ∈ ℋ ∧ w ∈ ℋ ) → (y +v (w −v w)) = y)
27	22, 26	eqtr3d 1130	. . . . . . . . . 10 ⊢ ((y ∈ ℋ ∧ w ∈ ℋ ) → (w +v (y −v w)) = y)
28	27	adantrl 311	. . . . . . . . 9 ⊢ ((y ∈ ℋ ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → (w +v (y −v w)) = y)
29	28	adantll 309	. . . . . . . 8 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → (w +v (y −v w)) = y)
30	29	adantlr 310	. . . . . . 7 ⊢ ((((x ∈ ℋ ∧ y ∈ ℋ ) ∧ v ∈ ℋ ) ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → (w +v (y −v w)) = y)
31	19, 30	syl 12	. . . . . 6 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (w +v (y −v w)) = y)
32	6, 11	shsva 5334	. . . . . . 7 ⊢ ((w ∈ S ∧ (y −v w) ∈ ((B +ℋ C) ∩ (R +ℋ S))) → (w +v (y −v w)) ∈ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))
33		pm3.27 260	. . . . . . . 8 ⊢ ((z ∈ C ∧ w ∈ S) → w ∈ S)
34	33	ad2antrl 322	. . . . . . 7 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → w ∈ S)
35		cleq1 1107	. . . . . . . . . . . . . . 15 ⊢ (v = (x +v y) → (v = (z +v w) ↔ (x +v y) = (z +v w)))
36	35	biimpa 324	. . . . . . . . . . . . . 14 ⊢ ((v = (x +v y) ∧ v = (z +v w)) → (x +v y) = (z +v w))
37	36	opreq1d 3012	. . . . . . . . . . . . 13 ⊢ ((v = (x +v y) ∧ v = (z +v w)) → ((x +v y) −v (x +v w)) = ((z +v w) −v (x +v w)))
38	37	adantrl 311	. . . . . . . . . . . 12 ⊢ ((v = (x +v y) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → ((x +v y) −v (x +v w)) = ((z +v w) −v (x +v w)))
39	38	adantll 309	. . . . . . . . . . 11 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → ((x +v y) −v (x +v w)) = ((z +v w) −v (x +v w)))
40		hvsub4t 5014	. . . . . . . . . . . . . . . 16 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ (x ∈ ℋ ∧ w ∈ ℋ )) → ((x +v y) −v (x +v w)) = ((x −v x) +v (y −v w)))
41		pm3.26 256	. . . . . . . . . . . . . . . 16 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ w ∈ ℋ ) → (x ∈ ℋ ∧ y ∈ ℋ ))
42		pm3.26 256	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ ℋ ∧ y ∈ ℋ ) → x ∈ ℋ )
43	42	anim1i 269	. . . . . . . . . . . . . . . 16 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ w ∈ ℋ ) → (x ∈ ℋ ∧ w ∈ ℋ ))
44	40, 41, 43	sylanc 361	. . . . . . . . . . . . . . 15 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ w ∈ ℋ ) → ((x +v y) −v (x +v w)) = ((x −v x) +v (y −v w)))
45		hvsubidt 5005	. . . . . . . . . . . . . . . . 17 ⊢ (x ∈ ℋ → (x −v x) = 0v)
46	45	ad2antll 320	. . . . . . . . . . . . . . . 16 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ w ∈ ℋ ) → (x −v x) = 0v)
47	46	opreq1d 3012	. . . . . . . . . . . . . . 15 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ w ∈ ℋ ) → ((x −v x) +v (y −v w)) = (0v +v (y −v w)))
48		hvsubclt 4998	. . . . . . . . . . . . . . . . 17 ⊢ ((y ∈ ℋ ∧ w ∈ ℋ ) → (y −v w) ∈ ℋ )
49		hvaddid2t 5003	. . . . . . . . . . . . . . . . 17 ⊢ ((y −v w) ∈ ℋ → (0v +v (y −v w)) = (y −v w))
50	48, 49	syl 12	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ ℋ ∧ w ∈ ℋ ) → (0v +v (y −v w)) = (y −v w))
51	50	adantll 309	. . . . . . . . . . . . . . 15 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ w ∈ ℋ ) → (0v +v (y −v w)) = (y −v w))
52	44, 47, 51	3eqtrd 1132	. . . . . . . . . . . . . 14 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ w ∈ ℋ ) → ((x +v y) −v (x +v w)) = (y −v w))
53	52	adantrl 311	. . . . . . . . . . . . 13 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → ((x +v y) −v (x +v w)) = (y −v w))
54	53	adantlr 310	. . . . . . . . . . . 12 ⊢ ((((x ∈ ℋ ∧ y ∈ ℋ ) ∧ v ∈ ℋ ) ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → ((x +v y) −v (x +v w)) = (y −v w))
55	19, 54	syl 12	. . . . . . . . . . 11 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → ((x +v y) −v (x +v w)) = (y −v w))
56		hvsub4t 5014	. . . . . . . . . . . . . . . 16 ⊢ (((z ∈ ℋ ∧ w ∈ ℋ ) ∧ (x ∈ ℋ ∧ w ∈ ℋ )) → ((z +v w) −v (x +v w)) = ((z −v x) +v (w −v w)))
57		pm3.27 260	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ ℋ ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → (z ∈ ℋ ∧ w ∈ ℋ ))
58		pm3.27 260	. . . . . . . . . . . . . . . . 17 ⊢ ((z ∈ ℋ ∧ w ∈ ℋ ) → w ∈ ℋ )
59	58	anim2i 270	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ ℋ ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → (x ∈ ℋ ∧ w ∈ ℋ ))
60	56, 57, 59	sylanc 361	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ ℋ ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → ((z +v w) −v (x +v w)) = ((z −v x) +v (w −v w)))
61	23	ad2antrr 323	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ ℋ ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → (w −v w) = 0v)
62	61	opreq2d 3013	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ ℋ ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → ((z −v x) +v (w −v w)) = ((z −v x) +v 0v))
63		hvsubclt 4998	. . . . . . . . . . . . . . . . . 18 ⊢ ((z ∈ ℋ ∧ x ∈ ℋ ) → (z −v x) ∈ ℋ )
64		ax-hvaddid 4988	. . . . . . . . . . . . . . . . . 18 ⊢ ((z −v x) ∈ ℋ → ((z −v x) +v 0v) = (z −v x))
65	63, 64	syl 12	. . . . . . . . . . . . . . . . 17 ⊢ ((z ∈ ℋ ∧ x ∈ ℋ ) → ((z −v x) +v 0v) = (z −v x))
66	65	ancoms 334	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ ℋ ∧ z ∈ ℋ ) → ((z −v x) +v 0v) = (z −v x))
67	66	adantrr 312	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ ℋ ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → ((z −v x) +v 0v) = (z −v x))
68	60, 62, 67	3eqtrd 1132	. . . . . . . . . . . . . 14 ⊢ ((x ∈ ℋ ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → ((z +v w) −v (x +v w)) = (z −v x))
69	68	adantlr 310	. . . . . . . . . . . . 13 ⊢ (((x ∈ ℋ ∧ y ∈ ℋ ) ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → ((z +v w) −v (x +v w)) = (z −v x))
70	69	adantlr 310	. . . . . . . . . . . 12 ⊢ ((((x ∈ ℋ ∧ y ∈ ℋ ) ∧ v ∈ ℋ ) ∧ (z ∈ ℋ ∧ w ∈ ℋ )) → ((z +v w) −v (x +v w)) = (z −v x))
71	19, 70	syl 12	. . . . . . . . . . 11 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → ((z +v w) −v (x +v w)) = (z −v x))
72	39, 55, 71	3eqtr3d 1133	. . . . . . . . . 10 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (y −v w) = (z −v x))
73	8, 2	shsvs 5337	. . . . . . . . . . . 12 ⊢ ((z ∈ C ∧ x ∈ B) → (z −v x) ∈ (C +ℋ B))
74		ancom 333	. . . . . . . . . . . 12 ⊢ ((x ∈ B ∧ z ∈ C) ↔ (z ∈ C ∧ x ∈ B))
75	2, 8	shscom 5333	. . . . . . . . . . . . 13 ⊢ (B +ℋ C) = (C +ℋ B)
76	75	eleq2i 1153	. . . . . . . . . . . 12 ⊢ ((z −v x) ∈ (B +ℋ C) ↔ (z −v x) ∈ (C +ℋ B))
77	73, 74, 76	3imtr4 192	. . . . . . . . . . 11 ⊢ ((x ∈ B ∧ z ∈ C) → (z −v x) ∈ (B +ℋ C))
78	15	adantr 306	. . . . . . . . . . 11 ⊢ (((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) → x ∈ B)
79		pm3.26 256	. . . . . . . . . . . 12 ⊢ ((z ∈ C ∧ w ∈ S) → z ∈ C)
80	79	adantr 306	. . . . . . . . . . 11 ⊢ (((z ∈ C ∧ w ∈ S) ∧ v = (z +v w)) → z ∈ C)
81	77, 78, 80	syl2an 349	. . . . . . . . . 10 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (z −v x) ∈ (B +ℋ C))
82	72, 81	eqeltrd 1163	. . . . . . . . 9 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (y −v w) ∈ (B +ℋ C))
83	4, 6	shsvs 5337	. . . . . . . . . 10 ⊢ ((y ∈ R ∧ w ∈ S) → (y −v w) ∈ (R +ℋ S))
84	17	adantr 306	. . . . . . . . . 10 ⊢ (((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) → y ∈ R)
85	33	adantr 306	. . . . . . . . . 10 ⊢ (((z ∈ C ∧ w ∈ S) ∧ v = (z +v w)) → w ∈ S)
86	83, 84, 85	syl2an 349	. . . . . . . . 9 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (y −v w) ∈ (R +ℋ S))
87	82, 86	jca 236	. . . . . . . 8 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → ((y −v w) ∈ (B +ℋ C) ∧ (y −v w) ∈ (R +ℋ S)))
88		elin 1635	. . . . . . . 8 ⊢ ((y −v w) ∈ ((B +ℋ C) ∩ (R +ℋ S)) ↔ ((y −v w) ∈ (B +ℋ C) ∧ (y −v w) ∈ (R +ℋ S)))
89	87, 88	sylibr 175	. . . . . . 7 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (y −v w) ∈ ((B +ℋ C) ∩ (R +ℋ S)))
90	32, 34, 89	sylanc 361	. . . . . 6 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (w +v (y −v w)) ∈ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))
91	31, 90	eqeltrrd 1164	. . . . 5 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → y ∈ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))
92	18, 91	jca 236	. . . 4 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (y ∈ R ∧ y ∈ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S)))))
93		elin 1635	. . . 4 ⊢ (y ∈ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S)))) ↔ (y ∈ R ∧ y ∈ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S)))))
94	92, 93	sylibr 175	. . 3 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → y ∈ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S)))))
95	14, 16, 94	sylanc 361	. 2 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (x +v y) ∈ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))))
96		eleq1 1149	. . 3 ⊢ (v = (x +v y) → (v ∈ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))) ↔ (x +v y) ∈ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S)))))))
97	96	ad2antlr 321	. 2 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → (v ∈ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))) ↔ (x +v y) ∈ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S)))))))
98	95, 97	mpbird 171	1 ⊢ ((((x ∈ B ∧ y ∈ R) ∧ v = (x +v y)) ∧ ((z ∈ C ∧ w ∈ S) ∧ v = (z +v w))) → v ∈ (B +ℋ (R ∩ (S +ℋ ((B +ℋ C) ∩ (R +ℋ S))))))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   = wceq 1091   ∈ wcel 1092   ∩ cin 1486  (class class class)co 3001   ℋ chil 4958   +_v cva 4959  0_vc0v 4961   −_v cmv 4962   C_ℋ cch 4968   +_ℋ cph 4970

This theorem is referenced by:  3oalem3 5554

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  ax-hilex 4983  ax-hvaddcl 4984  ax-hvcom 4985  ax-hvass 4986  ax-hvzercl 4987  ax-hvaddid 4988  ax-hvmulcl 4989  ax-hvmulid 4991  ax-hvdistr1 4993  ax-hvdistr2 4994  ax-hvmulzer 4995

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-1p 3881  df-plp 3882  df-mp 3883  df-ltp 3884  df-plpr 3958  df-mpr 3959  df-enr 3960  df-nr 3961  df-plr 3962  df-mr 3963  df-0r 3965  df-1r 3966  df-m1r 3967  df-c 4034  df-0 4035  df-1 4036  df-r 4038  df-plus 4039  df-sub 4133  df-neg 4135  df-hvsub 4996  df-sh 5114  df-ch 5127  df-shsum 5275

metamath.org