Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  usgrexmplef Structured version   Visualization version   GIF version

Theorem usgrexmplef 26196
 Description: Lemma for usgrexmpl 26200. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
Hypotheses
Ref Expression
usgrexmplef.v 𝑉 = (0...4)
usgrexmplef.e 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩
Assertion
Ref Expression
usgrexmplef 𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}
Distinct variable groups:   𝑒,𝐸   𝑒,𝑉

Proof of Theorem usgrexmplef
Dummy variables 𝑥 𝑦 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 usgrexmpldifpr 26195 . . 3 (({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3}))
2 usgrexmplef.e . . 3 𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩
3 prex 4939 . . . 4 {0, 1} ∈ V
4 prex 4939 . . . 4 {1, 2} ∈ V
5 prex 4939 . . . 4 {2, 0} ∈ V
6 prex 4939 . . . 4 {0, 3} ∈ V
7 s4f1o 13709 . . . 4 ((({0, 1} ∈ V ∧ {1, 2} ∈ V) ∧ ({2, 0} ∈ V ∧ {0, 3} ∈ V)) → ((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3})) → (𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩ → 𝐸:dom 𝐸1-1-onto→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}))))
83, 4, 5, 6, 7mp4an 709 . . 3 ((({0, 1} ≠ {1, 2} ∧ {0, 1} ≠ {2, 0} ∧ {0, 1} ≠ {0, 3}) ∧ ({1, 2} ≠ {2, 0} ∧ {1, 2} ≠ {0, 3} ∧ {2, 0} ≠ {0, 3})) → (𝐸 = ⟨“{0, 1} {1, 2} {2, 0} {0, 3}”⟩ → 𝐸:dom 𝐸1-1-onto→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})))
91, 2, 8mp2 9 . 2 𝐸:dom 𝐸1-1-onto→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})
10 f1of1 6174 . 2 (𝐸:dom 𝐸1-1-onto→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → 𝐸:dom 𝐸1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}))
11 id 22 . . . . . . 7 (ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}))
12 vex 3234 . . . . . . . . . . . 12 𝑝 ∈ V
1312elpr 4231 . . . . . . . . . . 11 (𝑝 ∈ {{0, 1}, {1, 2}} ↔ (𝑝 = {0, 1} ∨ 𝑝 = {1, 2}))
14 0nn0 11345 . . . . . . . . . . . . . . . 16 0 ∈ ℕ0
15 4nn0 11349 . . . . . . . . . . . . . . . 16 4 ∈ ℕ0
16 0re 10078 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
17 4re 11135 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ
18 4pos 11154 . . . . . . . . . . . . . . . . 17 0 < 4
1916, 17, 18ltleii 10198 . . . . . . . . . . . . . . . 16 0 ≤ 4
20 elfz2nn0 12469 . . . . . . . . . . . . . . . 16 (0 ∈ (0...4) ↔ (0 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 0 ≤ 4))
2114, 15, 19, 20mpbir3an 1263 . . . . . . . . . . . . . . 15 0 ∈ (0...4)
22 usgrexmplef.v . . . . . . . . . . . . . . 15 𝑉 = (0...4)
2321, 22eleqtrri 2729 . . . . . . . . . . . . . 14 0 ∈ 𝑉
24 1nn0 11346 . . . . . . . . . . . . . . . 16 1 ∈ ℕ0
25 1re 10077 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
26 1lt4 11237 . . . . . . . . . . . . . . . . 17 1 < 4
2725, 17, 26ltleii 10198 . . . . . . . . . . . . . . . 16 1 ≤ 4
28 elfz2nn0 12469 . . . . . . . . . . . . . . . 16 (1 ∈ (0...4) ↔ (1 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 1 ≤ 4))
2924, 15, 27, 28mpbir3an 1263 . . . . . . . . . . . . . . 15 1 ∈ (0...4)
3029, 22eleqtrri 2729 . . . . . . . . . . . . . 14 1 ∈ 𝑉
31 prelpwi 4945 . . . . . . . . . . . . . . 15 ((0 ∈ 𝑉 ∧ 1 ∈ 𝑉) → {0, 1} ∈ 𝒫 𝑉)
32 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑝 = {0, 1} → (𝑝 ∈ 𝒫 𝑉 ↔ {0, 1} ∈ 𝒫 𝑉))
3331, 32syl5ibrcom 237 . . . . . . . . . . . . . 14 ((0 ∈ 𝑉 ∧ 1 ∈ 𝑉) → (𝑝 = {0, 1} → 𝑝 ∈ 𝒫 𝑉))
3423, 30, 33mp2an 708 . . . . . . . . . . . . 13 (𝑝 = {0, 1} → 𝑝 ∈ 𝒫 𝑉)
35 fveq2 6229 . . . . . . . . . . . . . 14 (𝑝 = {0, 1} → (#‘𝑝) = (#‘{0, 1}))
36 prhash2ex 13225 . . . . . . . . . . . . . 14 (#‘{0, 1}) = 2
3735, 36syl6eq 2701 . . . . . . . . . . . . 13 (𝑝 = {0, 1} → (#‘𝑝) = 2)
3834, 37jca 553 . . . . . . . . . . . 12 (𝑝 = {0, 1} → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2))
39 2nn0 11347 . . . . . . . . . . . . . . . 16 2 ∈ ℕ0
40 2re 11128 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
41 2lt4 11236 . . . . . . . . . . . . . . . . 17 2 < 4
4240, 17, 41ltleii 10198 . . . . . . . . . . . . . . . 16 2 ≤ 4
43 elfz2nn0 12469 . . . . . . . . . . . . . . . 16 (2 ∈ (0...4) ↔ (2 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 2 ≤ 4))
4439, 15, 42, 43mpbir3an 1263 . . . . . . . . . . . . . . 15 2 ∈ (0...4)
4544, 22eleqtrri 2729 . . . . . . . . . . . . . 14 2 ∈ 𝑉
46 prelpwi 4945 . . . . . . . . . . . . . . 15 ((1 ∈ 𝑉 ∧ 2 ∈ 𝑉) → {1, 2} ∈ 𝒫 𝑉)
47 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑝 = {1, 2} → (𝑝 ∈ 𝒫 𝑉 ↔ {1, 2} ∈ 𝒫 𝑉))
4846, 47syl5ibrcom 237 . . . . . . . . . . . . . 14 ((1 ∈ 𝑉 ∧ 2 ∈ 𝑉) → (𝑝 = {1, 2} → 𝑝 ∈ 𝒫 𝑉))
4930, 45, 48mp2an 708 . . . . . . . . . . . . 13 (𝑝 = {1, 2} → 𝑝 ∈ 𝒫 𝑉)
50 fveq2 6229 . . . . . . . . . . . . . 14 (𝑝 = {1, 2} → (#‘𝑝) = (#‘{1, 2}))
51 1ne2 11278 . . . . . . . . . . . . . . 15 1 ≠ 2
52 1nn 11069 . . . . . . . . . . . . . . . 16 1 ∈ ℕ
53 2nn 11223 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
54 hashprg 13220 . . . . . . . . . . . . . . . 16 ((1 ∈ ℕ ∧ 2 ∈ ℕ) → (1 ≠ 2 ↔ (#‘{1, 2}) = 2))
5552, 53, 54mp2an 708 . . . . . . . . . . . . . . 15 (1 ≠ 2 ↔ (#‘{1, 2}) = 2)
5651, 55mpbi 220 . . . . . . . . . . . . . 14 (#‘{1, 2}) = 2
5750, 56syl6eq 2701 . . . . . . . . . . . . 13 (𝑝 = {1, 2} → (#‘𝑝) = 2)
5849, 57jca 553 . . . . . . . . . . . 12 (𝑝 = {1, 2} → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2))
5938, 58jaoi 393 . . . . . . . . . . 11 ((𝑝 = {0, 1} ∨ 𝑝 = {1, 2}) → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2))
6013, 59sylbi 207 . . . . . . . . . 10 (𝑝 ∈ {{0, 1}, {1, 2}} → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2))
6112elpr 4231 . . . . . . . . . . 11 (𝑝 ∈ {{2, 0}, {0, 3}} ↔ (𝑝 = {2, 0} ∨ 𝑝 = {0, 3}))
62 prelpwi 4945 . . . . . . . . . . . . . . 15 ((2 ∈ 𝑉 ∧ 0 ∈ 𝑉) → {2, 0} ∈ 𝒫 𝑉)
63 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑝 = {2, 0} → (𝑝 ∈ 𝒫 𝑉 ↔ {2, 0} ∈ 𝒫 𝑉))
6462, 63syl5ibrcom 237 . . . . . . . . . . . . . 14 ((2 ∈ 𝑉 ∧ 0 ∈ 𝑉) → (𝑝 = {2, 0} → 𝑝 ∈ 𝒫 𝑉))
6545, 23, 64mp2an 708 . . . . . . . . . . . . 13 (𝑝 = {2, 0} → 𝑝 ∈ 𝒫 𝑉)
66 fveq2 6229 . . . . . . . . . . . . . 14 (𝑝 = {2, 0} → (#‘𝑝) = (#‘{2, 0}))
67 2ne0 11151 . . . . . . . . . . . . . . 15 2 ≠ 0
68 2z 11447 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
69 0z 11426 . . . . . . . . . . . . . . . 16 0 ∈ ℤ
70 hashprg 13220 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 0 ∈ ℤ) → (2 ≠ 0 ↔ (#‘{2, 0}) = 2))
7168, 69, 70mp2an 708 . . . . . . . . . . . . . . 15 (2 ≠ 0 ↔ (#‘{2, 0}) = 2)
7267, 71mpbi 220 . . . . . . . . . . . . . 14 (#‘{2, 0}) = 2
7366, 72syl6eq 2701 . . . . . . . . . . . . 13 (𝑝 = {2, 0} → (#‘𝑝) = 2)
7465, 73jca 553 . . . . . . . . . . . 12 (𝑝 = {2, 0} → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2))
75 3nn0 11348 . . . . . . . . . . . . . . . 16 3 ∈ ℕ0
76 3re 11132 . . . . . . . . . . . . . . . . 17 3 ∈ ℝ
77 3lt4 11235 . . . . . . . . . . . . . . . . 17 3 < 4
7876, 17, 77ltleii 10198 . . . . . . . . . . . . . . . 16 3 ≤ 4
79 elfz2nn0 12469 . . . . . . . . . . . . . . . 16 (3 ∈ (0...4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 3 ≤ 4))
8075, 15, 78, 79mpbir3an 1263 . . . . . . . . . . . . . . 15 3 ∈ (0...4)
8180, 22eleqtrri 2729 . . . . . . . . . . . . . 14 3 ∈ 𝑉
82 prelpwi 4945 . . . . . . . . . . . . . . 15 ((0 ∈ 𝑉 ∧ 3 ∈ 𝑉) → {0, 3} ∈ 𝒫 𝑉)
83 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑝 = {0, 3} → (𝑝 ∈ 𝒫 𝑉 ↔ {0, 3} ∈ 𝒫 𝑉))
8482, 83syl5ibrcom 237 . . . . . . . . . . . . . 14 ((0 ∈ 𝑉 ∧ 3 ∈ 𝑉) → (𝑝 = {0, 3} → 𝑝 ∈ 𝒫 𝑉))
8523, 81, 84mp2an 708 . . . . . . . . . . . . 13 (𝑝 = {0, 3} → 𝑝 ∈ 𝒫 𝑉)
86 fveq2 6229 . . . . . . . . . . . . . 14 (𝑝 = {0, 3} → (#‘𝑝) = (#‘{0, 3}))
87 3ne0 11153 . . . . . . . . . . . . . . . 16 3 ≠ 0
8887necomi 2877 . . . . . . . . . . . . . . 15 0 ≠ 3
89 3z 11448 . . . . . . . . . . . . . . . 16 3 ∈ ℤ
90 hashprg 13220 . . . . . . . . . . . . . . . 16 ((0 ∈ ℤ ∧ 3 ∈ ℤ) → (0 ≠ 3 ↔ (#‘{0, 3}) = 2))
9169, 89, 90mp2an 708 . . . . . . . . . . . . . . 15 (0 ≠ 3 ↔ (#‘{0, 3}) = 2)
9288, 91mpbi 220 . . . . . . . . . . . . . 14 (#‘{0, 3}) = 2
9386, 92syl6eq 2701 . . . . . . . . . . . . 13 (𝑝 = {0, 3} → (#‘𝑝) = 2)
9485, 93jca 553 . . . . . . . . . . . 12 (𝑝 = {0, 3} → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2))
9574, 94jaoi 393 . . . . . . . . . . 11 ((𝑝 = {2, 0} ∨ 𝑝 = {0, 3}) → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2))
9661, 95sylbi 207 . . . . . . . . . 10 (𝑝 ∈ {{2, 0}, {0, 3}} → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2))
9760, 96jaoi 393 . . . . . . . . 9 ((𝑝 ∈ {{0, 1}, {1, 2}} ∨ 𝑝 ∈ {{2, 0}, {0, 3}}) → (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2))
98 elun 3786 . . . . . . . . 9 (𝑝 ∈ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ↔ (𝑝 ∈ {{0, 1}, {1, 2}} ∨ 𝑝 ∈ {{2, 0}, {0, 3}}))
99 fveq2 6229 . . . . . . . . . . 11 (𝑒 = 𝑝 → (#‘𝑒) = (#‘𝑝))
10099eqeq1d 2653 . . . . . . . . . 10 (𝑒 = 𝑝 → ((#‘𝑒) = 2 ↔ (#‘𝑝) = 2))
101100elrab 3396 . . . . . . . . 9 (𝑝 ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ↔ (𝑝 ∈ 𝒫 𝑉 ∧ (#‘𝑝) = 2))
10297, 98, 1013imtr4i 281 . . . . . . . 8 (𝑝 ∈ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → 𝑝 ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2})
103102ssriv 3640 . . . . . . 7 ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}
10411, 103syl6ss 3648 . . . . . 6 (ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2})
105104anim2i 592 . . . . 5 ((𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})) → (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}))
106 df-f 5930 . . . . 5 (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ↔ (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})))
107 df-f 5930 . . . . 5 (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ↔ (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}))
108105, 106, 1073imtr4i 281 . . . 4 (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → 𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2})
109108anim1i 591 . . 3 ((𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥) → (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥))
110 dff12 6138 . . 3 (𝐸:dom 𝐸1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ↔ (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥))
111 dff12 6138 . . 3 (𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ↔ (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2} ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥))
112109, 110, 1113imtr4i 281 . 2 (𝐸:dom 𝐸1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → 𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2})
1139, 10, 112mp2b 10 1 𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (#‘𝑒) = 2}
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054  ∀wal 1521   = wceq 1523   ∈ wcel 2030  ∃*wmo 2499   ≠ wne 2823  {crab 2945  Vcvv 3231   ∪ cun 3605   ⊆ wss 3607  𝒫 cpw 4191  {cpr 4212   class class class wbr 4685  dom cdm 5143  ran crn 5144   Fn wfn 5921  ⟶wf 5922  –1-1→wf1 5923  –1-1-onto→wf1o 5925  ‘cfv 5926  (class class class)co 6690  0cc0 9974  1c1 9975   ≤ cle 10113  ℕcn 11058  2c2 11108  3c3 11109  4c4 11110  ℕ0cn0 11330  ℤcz 11415  ...cfz 12364  #chash 13157  ⟨“cs4 13634 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-hash 13158  df-word 13331  df-concat 13333  df-s1 13334  df-s2 13639  df-s3 13640  df-s4 13641 This theorem is referenced by:  usgrexmpl  26200
 Copyright terms: Public domain W3C validator