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

Theorem usgrexmplef 28445
Description: Lemma for usgrexmpl 28449. (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 28444 . . 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 5426 . . . 4 {0, 1} ∈ V
4 prex 5426 . . . 4 {1, 2} ∈ V
5 prex 5426 . . . 4 {2, 0} ∈ V
6 prex 5426 . . . 4 {0, 3} ∈ V
7 s4f1o 14853 . . . 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 691 . . 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 6820 . 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 3478 . . . . . . . . . . . 12 𝑝 ∈ V
1312elpr 4646 . . . . . . . . . . 11 (𝑝 ∈ {{0, 1}, {1, 2}} ↔ (𝑝 = {0, 1} ∨ 𝑝 = {1, 2}))
14 0nn0 12471 . . . . . . . . . . . . . . . 16 0 ∈ ℕ0
15 4nn0 12475 . . . . . . . . . . . . . . . 16 4 ∈ ℕ0
16 0re 11200 . . . . . . . . . . . . . . . . 17 0 ∈ ℝ
17 4re 12280 . . . . . . . . . . . . . . . . 17 4 ∈ ℝ
18 4pos 12303 . . . . . . . . . . . . . . . . 17 0 < 4
1916, 17, 18ltleii 11321 . . . . . . . . . . . . . . . 16 0 ≤ 4
20 elfz2nn0 13576 . . . . . . . . . . . . . . . 16 (0 ∈ (0...4) ↔ (0 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 0 ≤ 4))
2114, 15, 19, 20mpbir3an 1341 . . . . . . . . . . . . . . 15 0 ∈ (0...4)
22 usgrexmplef.v . . . . . . . . . . . . . . 15 𝑉 = (0...4)
2321, 22eleqtrri 2832 . . . . . . . . . . . . . 14 0 ∈ 𝑉
24 1nn0 12472 . . . . . . . . . . . . . . . 16 1 ∈ ℕ0
25 1re 11198 . . . . . . . . . . . . . . . . 17 1 ∈ ℝ
26 1lt4 12372 . . . . . . . . . . . . . . . . 17 1 < 4
2725, 17, 26ltleii 11321 . . . . . . . . . . . . . . . 16 1 ≤ 4
28 elfz2nn0 13576 . . . . . . . . . . . . . . . 16 (1 ∈ (0...4) ↔ (1 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 1 ≤ 4))
2924, 15, 27, 28mpbir3an 1341 . . . . . . . . . . . . . . 15 1 ∈ (0...4)
3029, 22eleqtrri 2832 . . . . . . . . . . . . . 14 1 ∈ 𝑉
31 prelpwi 5441 . . . . . . . . . . . . . . 15 ((0 ∈ 𝑉 ∧ 1 ∈ 𝑉) → {0, 1} ∈ 𝒫 𝑉)
32 eleq1 2821 . . . . . . . . . . . . . . 15 (𝑝 = {0, 1} → (𝑝 ∈ 𝒫 𝑉 ↔ {0, 1} ∈ 𝒫 𝑉))
3331, 32syl5ibrcom 246 . . . . . . . . . . . . . 14 ((0 ∈ 𝑉 ∧ 1 ∈ 𝑉) → (𝑝 = {0, 1} → 𝑝 ∈ 𝒫 𝑉))
3423, 30, 33mp2an 690 . . . . . . . . . . . . 13 (𝑝 = {0, 1} → 𝑝 ∈ 𝒫 𝑉)
35 fveq2 6879 . . . . . . . . . . . . . 14 (𝑝 = {0, 1} → (♯‘𝑝) = (♯‘{0, 1}))
36 prhash2ex 14343 . . . . . . . . . . . . . 14 (♯‘{0, 1}) = 2
3735, 36eqtrdi 2788 . . . . . . . . . . . . 13 (𝑝 = {0, 1} → (♯‘𝑝) = 2)
3834, 37jca 512 . . . . . . . . . . . 12 (𝑝 = {0, 1} → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2))
39 2nn0 12473 . . . . . . . . . . . . . . . 16 2 ∈ ℕ0
40 2re 12270 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
41 2lt4 12371 . . . . . . . . . . . . . . . . 17 2 < 4
4240, 17, 41ltleii 11321 . . . . . . . . . . . . . . . 16 2 ≤ 4
43 elfz2nn0 13576 . . . . . . . . . . . . . . . 16 (2 ∈ (0...4) ↔ (2 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 2 ≤ 4))
4439, 15, 42, 43mpbir3an 1341 . . . . . . . . . . . . . . 15 2 ∈ (0...4)
4544, 22eleqtrri 2832 . . . . . . . . . . . . . 14 2 ∈ 𝑉
46 prelpwi 5441 . . . . . . . . . . . . . . 15 ((1 ∈ 𝑉 ∧ 2 ∈ 𝑉) → {1, 2} ∈ 𝒫 𝑉)
47 eleq1 2821 . . . . . . . . . . . . . . 15 (𝑝 = {1, 2} → (𝑝 ∈ 𝒫 𝑉 ↔ {1, 2} ∈ 𝒫 𝑉))
4846, 47syl5ibrcom 246 . . . . . . . . . . . . . 14 ((1 ∈ 𝑉 ∧ 2 ∈ 𝑉) → (𝑝 = {1, 2} → 𝑝 ∈ 𝒫 𝑉))
4930, 45, 48mp2an 690 . . . . . . . . . . . . 13 (𝑝 = {1, 2} → 𝑝 ∈ 𝒫 𝑉)
50 fveq2 6879 . . . . . . . . . . . . . 14 (𝑝 = {1, 2} → (♯‘𝑝) = (♯‘{1, 2}))
51 1ne2 12404 . . . . . . . . . . . . . . 15 1 ≠ 2
52 1nn 12207 . . . . . . . . . . . . . . . 16 1 ∈ ℕ
53 2nn 12269 . . . . . . . . . . . . . . . 16 2 ∈ ℕ
54 hashprg 14339 . . . . . . . . . . . . . . . 16 ((1 ∈ ℕ ∧ 2 ∈ ℕ) → (1 ≠ 2 ↔ (♯‘{1, 2}) = 2))
5552, 53, 54mp2an 690 . . . . . . . . . . . . . . 15 (1 ≠ 2 ↔ (♯‘{1, 2}) = 2)
5651, 55mpbi 229 . . . . . . . . . . . . . 14 (♯‘{1, 2}) = 2
5750, 56eqtrdi 2788 . . . . . . . . . . . . 13 (𝑝 = {1, 2} → (♯‘𝑝) = 2)
5849, 57jca 512 . . . . . . . . . . . 12 (𝑝 = {1, 2} → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2))
5938, 58jaoi 855 . . . . . . . . . . 11 ((𝑝 = {0, 1} ∨ 𝑝 = {1, 2}) → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2))
6013, 59sylbi 216 . . . . . . . . . 10 (𝑝 ∈ {{0, 1}, {1, 2}} → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2))
6112elpr 4646 . . . . . . . . . . 11 (𝑝 ∈ {{2, 0}, {0, 3}} ↔ (𝑝 = {2, 0} ∨ 𝑝 = {0, 3}))
62 prelpwi 5441 . . . . . . . . . . . . . . 15 ((2 ∈ 𝑉 ∧ 0 ∈ 𝑉) → {2, 0} ∈ 𝒫 𝑉)
63 eleq1 2821 . . . . . . . . . . . . . . 15 (𝑝 = {2, 0} → (𝑝 ∈ 𝒫 𝑉 ↔ {2, 0} ∈ 𝒫 𝑉))
6462, 63syl5ibrcom 246 . . . . . . . . . . . . . 14 ((2 ∈ 𝑉 ∧ 0 ∈ 𝑉) → (𝑝 = {2, 0} → 𝑝 ∈ 𝒫 𝑉))
6545, 23, 64mp2an 690 . . . . . . . . . . . . 13 (𝑝 = {2, 0} → 𝑝 ∈ 𝒫 𝑉)
66 fveq2 6879 . . . . . . . . . . . . . 14 (𝑝 = {2, 0} → (♯‘𝑝) = (♯‘{2, 0}))
67 2ne0 12300 . . . . . . . . . . . . . . 15 2 ≠ 0
68 2z 12578 . . . . . . . . . . . . . . . 16 2 ∈ ℤ
69 0z 12553 . . . . . . . . . . . . . . . 16 0 ∈ ℤ
70 hashprg 14339 . . . . . . . . . . . . . . . 16 ((2 ∈ ℤ ∧ 0 ∈ ℤ) → (2 ≠ 0 ↔ (♯‘{2, 0}) = 2))
7168, 69, 70mp2an 690 . . . . . . . . . . . . . . 15 (2 ≠ 0 ↔ (♯‘{2, 0}) = 2)
7267, 71mpbi 229 . . . . . . . . . . . . . 14 (♯‘{2, 0}) = 2
7366, 72eqtrdi 2788 . . . . . . . . . . . . 13 (𝑝 = {2, 0} → (♯‘𝑝) = 2)
7465, 73jca 512 . . . . . . . . . . . 12 (𝑝 = {2, 0} → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2))
75 3nn0 12474 . . . . . . . . . . . . . . . 16 3 ∈ ℕ0
76 3re 12276 . . . . . . . . . . . . . . . . 17 3 ∈ ℝ
77 3lt4 12370 . . . . . . . . . . . . . . . . 17 3 < 4
7876, 17, 77ltleii 11321 . . . . . . . . . . . . . . . 16 3 ≤ 4
79 elfz2nn0 13576 . . . . . . . . . . . . . . . 16 (3 ∈ (0...4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 3 ≤ 4))
8075, 15, 78, 79mpbir3an 1341 . . . . . . . . . . . . . . 15 3 ∈ (0...4)
8180, 22eleqtrri 2832 . . . . . . . . . . . . . 14 3 ∈ 𝑉
82 prelpwi 5441 . . . . . . . . . . . . . . 15 ((0 ∈ 𝑉 ∧ 3 ∈ 𝑉) → {0, 3} ∈ 𝒫 𝑉)
83 eleq1 2821 . . . . . . . . . . . . . . 15 (𝑝 = {0, 3} → (𝑝 ∈ 𝒫 𝑉 ↔ {0, 3} ∈ 𝒫 𝑉))
8482, 83syl5ibrcom 246 . . . . . . . . . . . . . 14 ((0 ∈ 𝑉 ∧ 3 ∈ 𝑉) → (𝑝 = {0, 3} → 𝑝 ∈ 𝒫 𝑉))
8523, 81, 84mp2an 690 . . . . . . . . . . . . 13 (𝑝 = {0, 3} → 𝑝 ∈ 𝒫 𝑉)
86 fveq2 6879 . . . . . . . . . . . . . 14 (𝑝 = {0, 3} → (♯‘𝑝) = (♯‘{0, 3}))
87 3ne0 12302 . . . . . . . . . . . . . . . 16 3 ≠ 0
8887necomi 2995 . . . . . . . . . . . . . . 15 0 ≠ 3
89 3z 12579 . . . . . . . . . . . . . . . 16 3 ∈ ℤ
90 hashprg 14339 . . . . . . . . . . . . . . . 16 ((0 ∈ ℤ ∧ 3 ∈ ℤ) → (0 ≠ 3 ↔ (♯‘{0, 3}) = 2))
9169, 89, 90mp2an 690 . . . . . . . . . . . . . . 15 (0 ≠ 3 ↔ (♯‘{0, 3}) = 2)
9288, 91mpbi 229 . . . . . . . . . . . . . 14 (♯‘{0, 3}) = 2
9386, 92eqtrdi 2788 . . . . . . . . . . . . 13 (𝑝 = {0, 3} → (♯‘𝑝) = 2)
9485, 93jca 512 . . . . . . . . . . . 12 (𝑝 = {0, 3} → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2))
9574, 94jaoi 855 . . . . . . . . . . 11 ((𝑝 = {2, 0} ∨ 𝑝 = {0, 3}) → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2))
9661, 95sylbi 216 . . . . . . . . . 10 (𝑝 ∈ {{2, 0}, {0, 3}} → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2))
9760, 96jaoi 855 . . . . . . . . 9 ((𝑝 ∈ {{0, 1}, {1, 2}} ∨ 𝑝 ∈ {{2, 0}, {0, 3}}) → (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2))
98 elun 4145 . . . . . . . . 9 (𝑝 ∈ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ↔ (𝑝 ∈ {{0, 1}, {1, 2}} ∨ 𝑝 ∈ {{2, 0}, {0, 3}}))
99 fveqeq2 6888 . . . . . . . . . 10 (𝑒 = 𝑝 → ((♯‘𝑒) = 2 ↔ (♯‘𝑝) = 2))
10099elrab 3680 . . . . . . . . 9 (𝑝 ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ↔ (𝑝 ∈ 𝒫 𝑉 ∧ (♯‘𝑝) = 2))
10197, 98, 1003imtr4i 291 . . . . . . . 8 (𝑝 ∈ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → 𝑝 ∈ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})
102101ssriv 3983 . . . . . . 7 ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
10311, 102sstrdi 3991 . . . . . 6 (ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})
104103anim2i 617 . . . . 5 ((𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})) → (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}))
105 df-f 6537 . . . . 5 (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ↔ (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ ({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}})))
106 df-f 6537 . . . . 5 (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ↔ (𝐸 Fn dom 𝐸 ∧ ran 𝐸 ⊆ {𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}))
107104, 105, 1063imtr4i 291 . . . 4 (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → 𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})
108107anim1i 615 . . 3 ((𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥) → (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥))
109 dff12 6774 . . 3 (𝐸:dom 𝐸1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ↔ (𝐸:dom 𝐸⟶({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥))
110 dff12 6774 . . 3 (𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ↔ (𝐸:dom 𝐸⟶{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2} ∧ ∀𝑥∃*𝑦 𝑦𝐸𝑥))
111108, 109, 1103imtr4i 291 . 2 (𝐸:dom 𝐸1-1→({{0, 1}, {1, 2}} ∪ {{2, 0}, {0, 3}}) → 𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2})
1129, 10, 111mp2b 10 1 𝐸:dom 𝐸1-1→{𝑒 ∈ 𝒫 𝑉 ∣ (♯‘𝑒) = 2}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3a 1087  wal 1539   = wceq 1541  wcel 2106  ∃*wmo 2532  wne 2940  {crab 3432  Vcvv 3474  cun 3943  wss 3945  𝒫 cpw 4597  {cpr 4625   class class class wbr 5142  dom cdm 5670  ran crn 5671   Fn wfn 6528  wf 6529  1-1wf1 6530  1-1-ontowf1o 6532  cfv 6533  (class class class)co 7394  0cc0 11094  1c1 11095  cle 11233  cn 12196  2c2 12251  3c3 12252  4c4 12253  0cn0 12456  cz 12542  ...cfz 13468  chash 14274  ⟨“cs4 14778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709  ax-cnex 11150  ax-resscn 11151  ax-1cn 11152  ax-icn 11153  ax-addcl 11154  ax-addrcl 11155  ax-mulcl 11156  ax-mulrcl 11157  ax-mulcom 11158  ax-addass 11159  ax-mulass 11160  ax-distr 11161  ax-i2m1 11162  ax-1ne0 11163  ax-1rid 11164  ax-rnegex 11165  ax-rrecex 11166  ax-cnre 11167  ax-pre-lttri 11168  ax-pre-lttrn 11169  ax-pre-ltadd 11170  ax-pre-mulgt0 11171
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5568  df-eprel 5574  df-po 5582  df-so 5583  df-fr 5625  df-we 5627  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-om 7840  df-1st 7959  df-2nd 7960  df-frecs 8250  df-wrecs 8281  df-recs 8355  df-rdg 8394  df-1o 8450  df-oadd 8454  df-er 8688  df-en 8925  df-dom 8926  df-sdom 8927  df-fin 8928  df-dju 9880  df-card 9918  df-pnf 11234  df-mnf 11235  df-xr 11236  df-ltxr 11237  df-le 11238  df-sub 11430  df-neg 11431  df-nn 12197  df-2 12259  df-3 12260  df-4 12261  df-n0 12457  df-z 12543  df-uz 12807  df-fz 13469  df-fzo 13612  df-hash 14275  df-word 14449  df-concat 14505  df-s1 14530  df-s2 14783  df-s3 14784  df-s4 14785
This theorem is referenced by:  usgrexmpl  28449
  Copyright terms: Public domain W3C validator