Theorem ltsopq 3869

Description: 'Less than' is a strict ordering on positive fractions.

Assertion

Ref	Expression
ltsopq	⊢ <Q Or Q

Proof of Theorem ltsopq

Step	Hyp	Ref	Expression
1		df-nq 3832	. . 3 ⊢ Q = ((N × N) / ~Q )
2		breq1 2065	. . . . 5 ⊢ ([⟨x, y⟩] ~Q = f → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ f <Q [⟨z, w⟩] ~Q ))
3		cleq1 1107	. . . . . . 7 ⊢ ([⟨x, y⟩] ~Q = f → ([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ↔ f = [⟨z, w⟩] ~Q ))
4		breq2 2066	. . . . . . 7 ⊢ ([⟨x, y⟩] ~Q = f → ([⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q ↔ [⟨z, w⟩] ~Q <Q f))
5	3, 4	orbi12d 475	. . . . . 6 ⊢ ([⟨x, y⟩] ~Q = f → (([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q ) ↔ (f = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q f)))
6	5	negbid 463	. . . . 5 ⊢ ([⟨x, y⟩] ~Q = f → (¬ ([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q ) ↔ ¬ (f = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q f)))
7	2, 6	bibi12d 477	. . . 4 ⊢ ([⟨x, y⟩] ~Q = f → (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ ¬ ([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q )) ↔ (f <Q [⟨z, w⟩] ~Q ↔ ¬ (f = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q f))))
8	2	anbi1d 469	. . . . 5 ⊢ ([⟨x, y⟩] ~Q = f → (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) ↔ (f <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q )))
9		breq1 2065	. . . . 5 ⊢ ([⟨x, y⟩] ~Q = f → ([⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q ↔ f <Q [⟨v, u⟩] ~Q ))
10	8, 9	imbi12d 474	. . . 4 ⊢ ([⟨x, y⟩] ~Q = f → ((([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → [⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q ) ↔ ((f <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → f <Q [⟨v, u⟩] ~Q )))
11	7, 10	anbi12d 476	. . 3 ⊢ ([⟨x, y⟩] ~Q = f → ((([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ ¬ ([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q )) ∧ (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → [⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q )) ↔ ((f <Q [⟨z, w⟩] ~Q ↔ ¬ (f = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q f)) ∧ ((f <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → f <Q [⟨v, u⟩] ~Q ))))
12		breq2 2066	. . . . 5 ⊢ ([⟨z, w⟩] ~Q = g → (f <Q [⟨z, w⟩] ~Q ↔ f <Q g))
13		cleq2 1110	. . . . . . 7 ⊢ ([⟨z, w⟩] ~Q = g → (f = [⟨z, w⟩] ~Q ↔ f = g))
14		breq1 2065	. . . . . . 7 ⊢ ([⟨z, w⟩] ~Q = g → ([⟨z, w⟩] ~Q <Q f ↔ g <Q f))
15	13, 14	orbi12d 475	. . . . . 6 ⊢ ([⟨z, w⟩] ~Q = g → ((f = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q f) ↔ (f = g ∨ g <Q f)))
16	15	negbid 463	. . . . 5 ⊢ ([⟨z, w⟩] ~Q = g → (¬ (f = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q f) ↔ ¬ (f = g ∨ g <Q f)))
17	12, 16	bibi12d 477	. . . 4 ⊢ ([⟨z, w⟩] ~Q = g → ((f <Q [⟨z, w⟩] ~Q ↔ ¬ (f = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q f)) ↔ (f <Q g ↔ ¬ (f = g ∨ g <Q f))))
18		breq1 2065	. . . . . 6 ⊢ ([⟨z, w⟩] ~Q = g → ([⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ↔ g <Q [⟨v, u⟩] ~Q ))
19	12, 18	anbi12d 476	. . . . 5 ⊢ ([⟨z, w⟩] ~Q = g → ((f <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) ↔ (f <Q g ∧ g <Q [⟨v, u⟩] ~Q )))
20	19	imbi1d 465	. . . 4 ⊢ ([⟨z, w⟩] ~Q = g → (((f <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → f <Q [⟨v, u⟩] ~Q ) ↔ ((f <Q g ∧ g <Q [⟨v, u⟩] ~Q ) → f <Q [⟨v, u⟩] ~Q )))
21	17, 20	anbi12d 476	. . 3 ⊢ ([⟨z, w⟩] ~Q = g → (((f <Q [⟨z, w⟩] ~Q ↔ ¬ (f = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q f)) ∧ ((f <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → f <Q [⟨v, u⟩] ~Q )) ↔ ((f <Q g ↔ ¬ (f = g ∨ g <Q f)) ∧ ((f <Q g ∧ g <Q [⟨v, u⟩] ~Q ) → f <Q [⟨v, u⟩] ~Q ))))
22		breq2 2066	. . . . . 6 ⊢ ([⟨v, u⟩] ~Q = h → (g <Q [⟨v, u⟩] ~Q ↔ g <Q h))
23	22	anbi2d 468	. . . . 5 ⊢ ([⟨v, u⟩] ~Q = h → ((f <Q g ∧ g <Q [⟨v, u⟩] ~Q ) ↔ (f <Q g ∧ g <Q h)))
24		breq2 2066	. . . . 5 ⊢ ([⟨v, u⟩] ~Q = h → (f <Q [⟨v, u⟩] ~Q ↔ f <Q h))
25	23, 24	imbi12d 474	. . . 4 ⊢ ([⟨v, u⟩] ~Q = h → (((f <Q g ∧ g <Q [⟨v, u⟩] ~Q ) → f <Q [⟨v, u⟩] ~Q ) ↔ ((f <Q g ∧ g <Q h) → f <Q h)))
26	25	anbi2d 468	. . 3 ⊢ ([⟨v, u⟩] ~Q = h → (((f <Q g ↔ ¬ (f = g ∨ g <Q f)) ∧ ((f <Q g ∧ g <Q [⟨v, u⟩] ~Q ) → f <Q [⟨v, u⟩] ~Q )) ↔ ((f <Q g ↔ ¬ (f = g ∨ g <Q f)) ∧ ((f <Q g ∧ g <Q h) → f <Q h))))
27		ltsopi 3810	. . . . . . . . . 10 ⊢ <N Or N
28		sotric 2148	. . . . . . . . . 10 ⊢ (( <N Or N ∧ ((x ·N w) ∈ N ∧ (y ·N z) ∈ N)) → ((x ·N w) <N (y ·N z) ↔ ¬ ((x ·N w) = (y ·N z) ∨ (y ·N z) <N (x ·N w))))
29	27, 28	mpan 518	. . . . . . . . 9 ⊢ (((x ·N w) ∈ N ∧ (y ·N z) ∈ N) → ((x ·N w) <N (y ·N z) ↔ ¬ ((x ·N w) = (y ·N z) ∨ (y ·N z) <N (x ·N w))))
30		mulclpi 3815	. . . . . . . . 9 ⊢ ((x ∈ N ∧ w ∈ N) → (x ·N w) ∈ N)
31		mulclpi 3815	. . . . . . . . 9 ⊢ ((y ∈ N ∧ z ∈ N) → (y ·N z) ∈ N)
32	29, 30, 31	syl2an 349	. . . . . . . 8 ⊢ (((x ∈ N ∧ w ∈ N) ∧ (y ∈ N ∧ z ∈ N)) → ((x ·N w) <N (y ·N z) ↔ ¬ ((x ·N w) = (y ·N z) ∨ (y ·N z) <N (x ·N w))))
33	32	an42s 391	. . . . . . 7 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ((x ·N w) <N (y ·N z) ↔ ¬ ((x ·N w) = (y ·N z) ∨ (y ·N z) <N (x ·N w))))
34		enqeceq 3841	. . . . . . . . 9 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ↔ (x ·N w) = (y ·N 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	ordpipq 3850	. . . . . . . . . . 11 ⊢ ([⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q ↔ (z ·N y) <N (w ·N x))
40	35, 38	mulcompi 3818	. . . . . . . . . . . 12 ⊢ (z ·N y) = (y ·N z)
41	36, 37	mulcompi 3818	. . . . . . . . . . . 12 ⊢ (w ·N x) = (x ·N w)
42	40, 41	breq12i 2070	. . . . . . . . . . 11 ⊢ ((z ·N y) <N (w ·N x) ↔ (y ·N z) <N (x ·N w))
43	39, 42	bitr 151	. . . . . . . . . 10 ⊢ ([⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q ↔ (y ·N z) <N (x ·N w))
44	43	a1i 7	. . . . . . . . 9 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ([⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q ↔ (y ·N z) <N (x ·N w)))
45	34, 44	orbi12d 475	. . . . . . . 8 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → (([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q ) ↔ ((x ·N w) = (y ·N z) ∨ (y ·N z) <N (x ·N w))))
46	45	negbid 463	. . . . . . 7 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → (¬ ([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q ) ↔ ¬ ((x ·N w) = (y ·N z) ∨ (y ·N z) <N (x ·N w))))
47	33, 46	bitr4d 409	. . . . . 6 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ((x ·N w) <N (y ·N z) ↔ ¬ ([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q )))
48	37, 38, 35, 36	ordpipq 3850	. . . . . 6 ⊢ ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (x ·N w) <N (y ·N z))
49	47, 48	syl5bb 410	. . . . 5 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N)) → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ ¬ ([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q )))
50	49	3adant3 599	. . . 4 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ ¬ ([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q )))
51		oprex 3018	. . . . . . . . . . . 12 ⊢ (x ·N w) ∈ V
52		oprex 3018	. . . . . . . . . . . 12 ⊢ (y ·N z) ∈ V
53		visset 1350	. . . . . . . . . . . . 13 ⊢ f ∈ V
54		visset 1350	. . . . . . . . . . . . 13 ⊢ g ∈ V
55	53, 54	ltmpi 3825	. . . . . . . . . . . 12 ⊢ (h ∈ N → (f <N g ↔ (h ·N f) <N (h ·N g)))
56		visset 1350	. . . . . . . . . . . 12 ⊢ u ∈ V
57	53, 54	mulcompi 3818	. . . . . . . . . . . 12 ⊢ (f ·N g) = (g ·N f)
58	51, 52, 55, 56, 57	caoprord2 3071	. . . . . . . . . . 11 ⊢ (u ∈ N → ((x ·N w) <N (y ·N z) ↔ ((x ·N w) ·N u) <N ((y ·N z) ·N u)))
59	36, 56	mulasspi 3819	. . . . . . . . . . . 12 ⊢ ((x ·N w) ·N u) = (x ·N (w ·N u))
60	35, 56	mulasspi 3819	. . . . . . . . . . . 12 ⊢ ((y ·N z) ·N u) = (y ·N (z ·N u))
61	59, 60	breq12i 2070	. . . . . . . . . . 11 ⊢ (((x ·N w) ·N u) <N ((y ·N z) ·N u) ↔ (x ·N (w ·N u)) <N (y ·N (z ·N u)))
62	58, 61	syl6bb 414	. . . . . . . . . 10 ⊢ (u ∈ N → ((x ·N w) <N (y ·N z) ↔ (x ·N (w ·N u)) <N (y ·N (z ·N u))))
63	62, 48	syl5bb 410	. . . . . . . . 9 ⊢ (u ∈ N → ([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ (x ·N (w ·N u)) <N (y ·N (z ·N u))))
64		oprex 3018	. . . . . . . . . . 11 ⊢ (z ·N u) ∈ V
65		oprex 3018	. . . . . . . . . . 11 ⊢ (w ·N v) ∈ V
66	64, 65	ltmpi 3825	. . . . . . . . . 10 ⊢ (y ∈ N → ((z ·N u) <N (w ·N v) ↔ (y ·N (z ·N u)) <N (y ·N (w ·N v))))
67		visset 1350	. . . . . . . . . . 11 ⊢ v ∈ V
68	35, 36, 67, 56	ordpipq 3850	. . . . . . . . . 10 ⊢ ([⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ↔ (z ·N u) <N (w ·N v))
69	66, 68	syl5bb 410	. . . . . . . . 9 ⊢ (y ∈ N → ([⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ↔ (y ·N (z ·N u)) <N (y ·N (w ·N v))))
70	63, 69	bi2anan9r 479	. . . . . . . 8 ⊢ ((y ∈ N ∧ u ∈ N) → (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) ↔ ((x ·N (w ·N u)) <N (y ·N (z ·N u)) ∧ (y ·N (z ·N u)) <N (y ·N (w ·N v)))))
71		oprex 3018	. . . . . . . . . 10 ⊢ (x ·N (w ·N u)) ∈ V
72		ltrelpi 3811	. . . . . . . . . 10 ⊢ <N ⊆ (N × N)
73		oprex 3018	. . . . . . . . . 10 ⊢ (y ·N (z ·N u)) ∈ V
74		oprex 3018	. . . . . . . . . 10 ⊢ (y ·N (w ·N v)) ∈ V
75	71, 27, 72, 73, 74	sotri 2630	. . . . . . . . 9 ⊢ (((x ·N (w ·N u)) <N (y ·N (z ·N u)) ∧ (y ·N (z ·N u)) <N (y ·N (w ·N v))) → (x ·N (w ·N u)) <N (y ·N (w ·N v)))
76		oprex 3018	. . . . . . . . . . 11 ⊢ (x ·N u) ∈ V
77		dmmulpi 3813	. . . . . . . . . . 11 ⊢ dom ·N = (N × N)
78		0npi 3804	. . . . . . . . . . 11 ⊢ ¬ ∅ ∈ N
79		oprex 3018	. . . . . . . . . . . 12 ⊢ (y ·N v) ∈ V
80	76, 79	ltmpi 3825	. . . . . . . . . . 11 ⊢ (w ∈ N → ((x ·N u) <N (y ·N v) ↔ (w ·N (x ·N u)) <N (w ·N (y ·N v))))
81	76, 77, 72, 78, 80	ndmordi 3065	. . . . . . . . . 10 ⊢ ((w ·N (x ·N u)) <N (w ·N (y ·N v)) → (x ·N u) <N (y ·N v))
82		visset 1350	. . . . . . . . . . . . 13 ⊢ h ∈ V
83	54, 82	mulasspi 3819	. . . . . . . . . . . 12 ⊢ ((f ·N g) ·N h) = (f ·N (g ·N h))
84	37, 36, 56, 57, 83	caopr12 3075	. . . . . . . . . . 11 ⊢ (x ·N (w ·N u)) = (w ·N (x ·N u))
85	38, 36, 67, 57, 83	caopr12 3075	. . . . . . . . . . 11 ⊢ (y ·N (w ·N v)) = (w ·N (y ·N v))
86	84, 85	breq12i 2070	. . . . . . . . . 10 ⊢ ((x ·N (w ·N u)) <N (y ·N (w ·N v)) ↔ (w ·N (x ·N u)) <N (w ·N (y ·N v)))
87	37, 38, 67, 56	ordpipq 3850	. . . . . . . . . 10 ⊢ ([⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q ↔ (x ·N u) <N (y ·N v))
88	81, 86, 87	3imtr4 192	. . . . . . . . 9 ⊢ ((x ·N (w ·N u)) <N (y ·N (w ·N v)) → [⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q )
89	75, 88	syl 12	. . . . . . . 8 ⊢ (((x ·N (w ·N u)) <N (y ·N (z ·N u)) ∧ (y ·N (z ·N u)) <N (y ·N (w ·N v))) → [⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q )
90	70, 89	syl6bi 187	. . . . . . 7 ⊢ ((y ∈ N ∧ u ∈ N) → (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → [⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q ))
91	90	adantrl 311	. . . . . 6 ⊢ ((y ∈ N ∧ (v ∈ N ∧ u ∈ N)) → (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → [⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q ))
92	91	adantll 309	. . . . 5 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → [⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q ))
93	92	3adant2 598	. . . 4 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → [⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q ))
94	50, 93	jca 236	. . 3 ⊢ (((x ∈ N ∧ y ∈ N) ∧ (z ∈ N ∧ w ∈ N) ∧ (v ∈ N ∧ u ∈ N)) → (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ↔ ¬ ([⟨x, y⟩] ~Q = [⟨z, w⟩] ~Q ∨ [⟨z, w⟩] ~Q <Q [⟨x, y⟩] ~Q )) ∧ (([⟨x, y⟩] ~Q <Q [⟨z, w⟩] ~Q ∧ [⟨z, w⟩] ~Q <Q [⟨v, u⟩] ~Q ) → [⟨x, y⟩] ~Q <Q [⟨v, u⟩] ~Q )))
95	1, 11, 21, 26, 94	3ecoptocl 3241	. 2 ⊢ ((f ∈ Q ∧ g ∈ Q ∧ h ∈ Q) → ((f <Q g ↔ ¬ (f = g ∨ g <Q f)) ∧ ((f <Q g ∧ g <Q h) → f <Q h)))
96	95	so 2152	1 ⊢ <Q Or Q

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  Ncnpi 3766   ·_N cmi 3768   <_N clti 3769   ~_Q ceq 3772  Qcnq 3773   <_Q cltq 3778

This theorem is referenced by:  ltrpq 3879  prub 3892  genpnnp 3902  1pr 3911  distrlem4pr 3924  prlem934 3933  ltexprlem4 3939  reclem2pr 3951  reclem4pr 3953

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-oadd 3106  df-omul 3107  df-er 3200  df-ec 3202  df-qs 3205  df-ni 3794  df-mi 3796  df-lti 3797  df-enq 3831  df-nq 3832  df-ltq 3836

metamath.org