ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltsrprg GIF version

Theorem ltsrprg 7759
Description: Ordering of signed reals in terms of positive reals. (Contributed by Jim Kingdon, 2-Jan-2019.)
Assertion
Ref Expression
ltsrprg (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ([⟨𝐴, 𝐵⟩] ~R <R [⟨𝐶, 𝐷⟩] ~R ↔ (𝐴 +P 𝐷)<P (𝐵 +P 𝐶)))

Proof of Theorem ltsrprg
Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑣 𝑢 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 enrex 7749 . 2 ~R ∈ V
2 enrer 7747 . 2 ~R Er (P × P)
3 df-nr 7739 . 2 R = ((P × P) / ~R )
4 df-ltr 7742 . 2 <R = {⟨𝑥, 𝑦⟩ ∣ ((𝑥R𝑦R) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~R𝑦 = [⟨𝑣, 𝑢⟩] ~R ) ∧ (𝑧 +P 𝑢)<P (𝑤 +P 𝑣)))}
5 enreceq 7748 . . . . 5 (((𝑧P𝑤P) ∧ (𝐴P𝐵P)) → ([⟨𝑧, 𝑤⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ↔ (𝑧 +P 𝐵) = (𝑤 +P 𝐴)))
6 enreceq 7748 . . . . . 6 (((𝑣P𝑢P) ∧ (𝐶P𝐷P)) → ([⟨𝑣, 𝑢⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ↔ (𝑣 +P 𝐷) = (𝑢 +P 𝐶)))
7 eqcom 2189 . . . . . 6 ((𝑣 +P 𝐷) = (𝑢 +P 𝐶) ↔ (𝑢 +P 𝐶) = (𝑣 +P 𝐷))
86, 7bitrdi 196 . . . . 5 (((𝑣P𝑢P) ∧ (𝐶P𝐷P)) → ([⟨𝑣, 𝑢⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ↔ (𝑢 +P 𝐶) = (𝑣 +P 𝐷)))
95, 8bi2anan9 606 . . . 4 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (([⟨𝑧, 𝑤⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝑣, 𝑢⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) ↔ ((𝑧 +P 𝐵) = (𝑤 +P 𝐴) ∧ (𝑢 +P 𝐶) = (𝑣 +P 𝐷))))
10 oveq12 5897 . . . . . . 7 (((𝑧 +P 𝐵) = (𝑤 +P 𝐴) ∧ (𝑢 +P 𝐶) = (𝑣 +P 𝐷)) → ((𝑧 +P 𝐵) +P (𝑢 +P 𝐶)) = ((𝑤 +P 𝐴) +P (𝑣 +P 𝐷)))
1110adantl 277 . . . . . 6 (((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) ∧ ((𝑧 +P 𝐵) = (𝑤 +P 𝐴) ∧ (𝑢 +P 𝐶) = (𝑣 +P 𝐷))) → ((𝑧 +P 𝐵) +P (𝑢 +P 𝐶)) = ((𝑤 +P 𝐴) +P (𝑣 +P 𝐷)))
12 simprlr 538 . . . . . . . . . . 11 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → 𝑢P)
13 simplrr 536 . . . . . . . . . . 11 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → 𝐵P)
14 addcomprg 7590 . . . . . . . . . . . 12 ((𝑢P𝐵P) → (𝑢 +P 𝐵) = (𝐵 +P 𝑢))
1514oveq1d 5903 . . . . . . . . . . 11 ((𝑢P𝐵P) → ((𝑢 +P 𝐵) +P 𝐶) = ((𝐵 +P 𝑢) +P 𝐶))
1612, 13, 15syl2anc 411 . . . . . . . . . 10 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝑢 +P 𝐵) +P 𝐶) = ((𝐵 +P 𝑢) +P 𝐶))
17 simprrl 539 . . . . . . . . . . 11 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → 𝐶P)
18 addassprg 7591 . . . . . . . . . . 11 ((𝑢P𝐵P𝐶P) → ((𝑢 +P 𝐵) +P 𝐶) = (𝑢 +P (𝐵 +P 𝐶)))
1912, 13, 17, 18syl3anc 1248 . . . . . . . . . 10 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝑢 +P 𝐵) +P 𝐶) = (𝑢 +P (𝐵 +P 𝐶)))
20 addassprg 7591 . . . . . . . . . . 11 ((𝐵P𝑢P𝐶P) → ((𝐵 +P 𝑢) +P 𝐶) = (𝐵 +P (𝑢 +P 𝐶)))
2113, 12, 17, 20syl3anc 1248 . . . . . . . . . 10 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝐵 +P 𝑢) +P 𝐶) = (𝐵 +P (𝑢 +P 𝐶)))
2216, 19, 213eqtr3d 2228 . . . . . . . . 9 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝑢 +P (𝐵 +P 𝐶)) = (𝐵 +P (𝑢 +P 𝐶)))
2322oveq2d 5904 . . . . . . . 8 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝑧 +P (𝑢 +P (𝐵 +P 𝐶))) = (𝑧 +P (𝐵 +P (𝑢 +P 𝐶))))
24 simplll 533 . . . . . . . . 9 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → 𝑧P)
25 addclpr 7549 . . . . . . . . . . . . 13 ((𝑤P𝑣P) → (𝑤 +P 𝑣) ∈ P)
2625ad2ant2lr 510 . . . . . . . . . . . 12 (((𝑧P𝑤P) ∧ (𝑣P𝑢P)) → (𝑤 +P 𝑣) ∈ P)
27 addclpr 7549 . . . . . . . . . . . . 13 ((𝐵P𝐶P) → (𝐵 +P 𝐶) ∈ P)
2827ad2ant2lr 510 . . . . . . . . . . . 12 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → (𝐵 +P 𝐶) ∈ P)
2926, 28anim12ci 339 . . . . . . . . . . 11 ((((𝑧P𝑤P) ∧ (𝑣P𝑢P)) ∧ ((𝐴P𝐵P) ∧ (𝐶P𝐷P))) → ((𝐵 +P 𝐶) ∈ P ∧ (𝑤 +P 𝑣) ∈ P))
3029an4s 588 . . . . . . . . . 10 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝐵 +P 𝐶) ∈ P ∧ (𝑤 +P 𝑣) ∈ P))
3130simpld 112 . . . . . . . . 9 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝐵 +P 𝐶) ∈ P)
32 addassprg 7591 . . . . . . . . 9 ((𝑧P𝑢P ∧ (𝐵 +P 𝐶) ∈ P) → ((𝑧 +P 𝑢) +P (𝐵 +P 𝐶)) = (𝑧 +P (𝑢 +P (𝐵 +P 𝐶))))
3324, 12, 31, 32syl3anc 1248 . . . . . . . 8 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝑧 +P 𝑢) +P (𝐵 +P 𝐶)) = (𝑧 +P (𝑢 +P (𝐵 +P 𝐶))))
34 addclpr 7549 . . . . . . . . . 10 ((𝑢P𝐶P) → (𝑢 +P 𝐶) ∈ P)
3512, 17, 34syl2anc 411 . . . . . . . . 9 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝑢 +P 𝐶) ∈ P)
36 addassprg 7591 . . . . . . . . 9 ((𝑧P𝐵P ∧ (𝑢 +P 𝐶) ∈ P) → ((𝑧 +P 𝐵) +P (𝑢 +P 𝐶)) = (𝑧 +P (𝐵 +P (𝑢 +P 𝐶))))
3724, 13, 35, 36syl3anc 1248 . . . . . . . 8 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝑧 +P 𝐵) +P (𝑢 +P 𝐶)) = (𝑧 +P (𝐵 +P (𝑢 +P 𝐶))))
3823, 33, 373eqtr4d 2230 . . . . . . 7 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝑧 +P 𝑢) +P (𝐵 +P 𝐶)) = ((𝑧 +P 𝐵) +P (𝑢 +P 𝐶)))
3938adantr 276 . . . . . 6 (((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) ∧ ((𝑧 +P 𝐵) = (𝑤 +P 𝐴) ∧ (𝑢 +P 𝐶) = (𝑣 +P 𝐷))) → ((𝑧 +P 𝑢) +P (𝐵 +P 𝐶)) = ((𝑧 +P 𝐵) +P (𝑢 +P 𝐶)))
40 simprll 537 . . . . . . . . . . . 12 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → 𝑣P)
41 simplrl 535 . . . . . . . . . . . 12 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → 𝐴P)
42 addcomprg 7590 . . . . . . . . . . . 12 ((𝑣P𝐴P) → (𝑣 +P 𝐴) = (𝐴 +P 𝑣))
4340, 41, 42syl2anc 411 . . . . . . . . . . 11 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝑣 +P 𝐴) = (𝐴 +P 𝑣))
4443oveq1d 5903 . . . . . . . . . 10 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝑣 +P 𝐴) +P 𝐷) = ((𝐴 +P 𝑣) +P 𝐷))
45 simprrr 540 . . . . . . . . . . 11 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → 𝐷P)
46 addassprg 7591 . . . . . . . . . . 11 ((𝑣P𝐴P𝐷P) → ((𝑣 +P 𝐴) +P 𝐷) = (𝑣 +P (𝐴 +P 𝐷)))
4740, 41, 45, 46syl3anc 1248 . . . . . . . . . 10 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝑣 +P 𝐴) +P 𝐷) = (𝑣 +P (𝐴 +P 𝐷)))
48 addassprg 7591 . . . . . . . . . . 11 ((𝐴P𝑣P𝐷P) → ((𝐴 +P 𝑣) +P 𝐷) = (𝐴 +P (𝑣 +P 𝐷)))
4941, 40, 45, 48syl3anc 1248 . . . . . . . . . 10 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝐴 +P 𝑣) +P 𝐷) = (𝐴 +P (𝑣 +P 𝐷)))
5044, 47, 493eqtr3d 2228 . . . . . . . . 9 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝑣 +P (𝐴 +P 𝐷)) = (𝐴 +P (𝑣 +P 𝐷)))
5150oveq2d 5904 . . . . . . . 8 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝑤 +P (𝑣 +P (𝐴 +P 𝐷))) = (𝑤 +P (𝐴 +P (𝑣 +P 𝐷))))
52 simpllr 534 . . . . . . . . 9 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → 𝑤P)
53 addclpr 7549 . . . . . . . . . 10 ((𝐴P𝐷P) → (𝐴 +P 𝐷) ∈ P)
5441, 45, 53syl2anc 411 . . . . . . . . 9 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝐴 +P 𝐷) ∈ P)
55 addassprg 7591 . . . . . . . . 9 ((𝑤P𝑣P ∧ (𝐴 +P 𝐷) ∈ P) → ((𝑤 +P 𝑣) +P (𝐴 +P 𝐷)) = (𝑤 +P (𝑣 +P (𝐴 +P 𝐷))))
5652, 40, 54, 55syl3anc 1248 . . . . . . . 8 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝑤 +P 𝑣) +P (𝐴 +P 𝐷)) = (𝑤 +P (𝑣 +P (𝐴 +P 𝐷))))
57 addclpr 7549 . . . . . . . . . 10 ((𝑣P𝐷P) → (𝑣 +P 𝐷) ∈ P)
5840, 45, 57syl2anc 411 . . . . . . . . 9 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝑣 +P 𝐷) ∈ P)
59 addassprg 7591 . . . . . . . . 9 ((𝑤P𝐴P ∧ (𝑣 +P 𝐷) ∈ P) → ((𝑤 +P 𝐴) +P (𝑣 +P 𝐷)) = (𝑤 +P (𝐴 +P (𝑣 +P 𝐷))))
6052, 41, 58, 59syl3anc 1248 . . . . . . . 8 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝑤 +P 𝐴) +P (𝑣 +P 𝐷)) = (𝑤 +P (𝐴 +P (𝑣 +P 𝐷))))
6151, 56, 603eqtr4d 2230 . . . . . . 7 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → ((𝑤 +P 𝑣) +P (𝐴 +P 𝐷)) = ((𝑤 +P 𝐴) +P (𝑣 +P 𝐷)))
6261adantr 276 . . . . . 6 (((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) ∧ ((𝑧 +P 𝐵) = (𝑤 +P 𝐴) ∧ (𝑢 +P 𝐶) = (𝑣 +P 𝐷))) → ((𝑤 +P 𝑣) +P (𝐴 +P 𝐷)) = ((𝑤 +P 𝐴) +P (𝑣 +P 𝐷)))
6311, 39, 623eqtr4d 2230 . . . . 5 (((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) ∧ ((𝑧 +P 𝐵) = (𝑤 +P 𝐴) ∧ (𝑢 +P 𝐶) = (𝑣 +P 𝐷))) → ((𝑧 +P 𝑢) +P (𝐵 +P 𝐶)) = ((𝑤 +P 𝑣) +P (𝐴 +P 𝐷)))
6463ex 115 . . . 4 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (((𝑧 +P 𝐵) = (𝑤 +P 𝐴) ∧ (𝑢 +P 𝐶) = (𝑣 +P 𝐷)) → ((𝑧 +P 𝑢) +P (𝐵 +P 𝐶)) = ((𝑤 +P 𝑣) +P (𝐴 +P 𝐷))))
659, 64sylbid 150 . . 3 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (([⟨𝑧, 𝑤⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝑣, 𝑢⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) → ((𝑧 +P 𝑢) +P (𝐵 +P 𝐶)) = ((𝑤 +P 𝑣) +P (𝐴 +P 𝐷))))
66 ltaprg 7631 . . . . 5 ((𝑥P𝑦P𝑓P) → (𝑥<P 𝑦 ↔ (𝑓 +P 𝑥)<P (𝑓 +P 𝑦)))
6766adantl 277 . . . 4 (((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) ∧ (𝑥P𝑦P𝑓P)) → (𝑥<P 𝑦 ↔ (𝑓 +P 𝑥)<P (𝑓 +P 𝑦)))
68 addclpr 7549 . . . . 5 ((𝑧P𝑢P) → (𝑧 +P 𝑢) ∈ P)
6924, 12, 68syl2anc 411 . . . 4 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝑧 +P 𝑢) ∈ P)
7030simprd 114 . . . 4 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (𝑤 +P 𝑣) ∈ P)
71 addcomprg 7590 . . . . 5 ((𝑥P𝑦P) → (𝑥 +P 𝑦) = (𝑦 +P 𝑥))
7271adantl 277 . . . 4 (((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) ∧ (𝑥P𝑦P)) → (𝑥 +P 𝑦) = (𝑦 +P 𝑥))
7367, 69, 31, 70, 72, 54caovord3d 6058 . . 3 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (((𝑧 +P 𝑢) +P (𝐵 +P 𝐶)) = ((𝑤 +P 𝑣) +P (𝐴 +P 𝐷)) → ((𝑧 +P 𝑢)<P (𝑤 +P 𝑣) ↔ (𝐴 +P 𝐷)<P (𝐵 +P 𝐶))))
7465, 73syld 45 . 2 ((((𝑧P𝑤P) ∧ (𝐴P𝐵P)) ∧ ((𝑣P𝑢P) ∧ (𝐶P𝐷P))) → (([⟨𝑧, 𝑤⟩] ~R = [⟨𝐴, 𝐵⟩] ~R ∧ [⟨𝑣, 𝑢⟩] ~R = [⟨𝐶, 𝐷⟩] ~R ) → ((𝑧 +P 𝑢)<P (𝑤 +P 𝑣) ↔ (𝐴 +P 𝐷)<P (𝐵 +P 𝐶))))
751, 2, 3, 4, 74brecop 6638 1 (((𝐴P𝐵P) ∧ (𝐶P𝐷P)) → ([⟨𝐴, 𝐵⟩] ~R <R [⟨𝐶, 𝐷⟩] ~R ↔ (𝐴 +P 𝐷)<P (𝐵 +P 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 979   = wceq 1363  wcel 2158  cop 3607   class class class wbr 4015  (class class class)co 5888  [cec 6546  Pcnp 7303   +P cpp 7305  <P cltp 7307   ~R cer 7308  Rcnr 7309   <R cltr 7315
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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-coll 4130  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-iinf 4599
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 980  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-ral 2470  df-rex 2471  df-reu 2472  df-rab 2474  df-v 2751  df-sbc 2975  df-csb 3070  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-int 3857  df-iun 3900  df-br 4016  df-opab 4077  df-mpt 4078  df-tr 4114  df-eprel 4301  df-id 4305  df-po 4308  df-iso 4309  df-iord 4378  df-on 4380  df-suc 4383  df-iom 4602  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-rn 4649  df-res 4650  df-ima 4651  df-iota 5190  df-fun 5230  df-fn 5231  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235  df-fv 5236  df-ov 5891  df-oprab 5892  df-mpo 5893  df-1st 6154  df-2nd 6155  df-recs 6319  df-irdg 6384  df-1o 6430  df-2o 6431  df-oadd 6434  df-omul 6435  df-er 6548  df-ec 6550  df-qs 6554  df-ni 7316  df-pli 7317  df-mi 7318  df-lti 7319  df-plpq 7356  df-mpq 7357  df-enq 7359  df-nqqs 7360  df-plqqs 7361  df-mqqs 7362  df-1nqqs 7363  df-rq 7364  df-ltnqqs 7365  df-enq0 7436  df-nq0 7437  df-0nq0 7438  df-plq0 7439  df-mq0 7440  df-inp 7478  df-iplp 7480  df-iltp 7482  df-enr 7738  df-nr 7739  df-ltr 7742
This theorem is referenced by:  gt0srpr  7760  lttrsr  7774  ltposr  7775  ltsosr  7776  0lt1sr  7777  ltasrg  7782  aptisr  7791  mulextsr1  7793  archsr  7794  prsrlt  7799  ltpsrprg  7815  mappsrprg  7816  map2psrprg  7817  pitoregt0  7861
  Copyright terms: Public domain W3C validator