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

Theorem ennnfonelemim 11974
 Description: Lemma for ennnfone 11975. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.)
Assertion
Ref Expression
ennnfonelemim (𝐴 ≈ ℕ → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗))))
Distinct variable groups:   𝐴,𝑓,𝑗,𝑛   𝑥,𝐴,𝑦,𝑛   𝑓,𝑘,𝑗,𝑛   𝑦,𝑗
Allowed substitution hint:   𝐴(𝑘)

Proof of Theorem ennnfonelemim
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 nn0ennn 10238 . . . 4 0 ≈ ℕ
21ensymi 6684 . . 3 ℕ ≈ ℕ0
3 entr 6686 . . 3 ((𝐴 ≈ ℕ ∧ ℕ ≈ ℕ0) → 𝐴 ≈ ℕ0)
42, 3mpan2 422 . 2 (𝐴 ≈ ℕ → 𝐴 ≈ ℕ0)
5 bren 6649 . . . 4 (𝐴 ≈ ℕ0 ↔ ∃𝑔 𝑔:𝐴1-1-onto→ℕ0)
65biimpi 119 . . 3 (𝐴 ≈ ℕ0 → ∃𝑔 𝑔:𝐴1-1-onto→ℕ0)
7 f1of 5375 . . . . . . . . . . 11 (𝑔:𝐴1-1-onto→ℕ0𝑔:𝐴⟶ℕ0)
87adantr 274 . . . . . . . . . 10 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → 𝑔:𝐴⟶ℕ0)
9 simprl 521 . . . . . . . . . 10 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → 𝑥𝐴)
108, 9ffvelrnd 5564 . . . . . . . . 9 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → (𝑔𝑥) ∈ ℕ0)
1110nn0zd 9196 . . . . . . . 8 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → (𝑔𝑥) ∈ ℤ)
12 simprr 522 . . . . . . . . . 10 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → 𝑦𝐴)
138, 12ffvelrnd 5564 . . . . . . . . 9 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → (𝑔𝑦) ∈ ℕ0)
1413nn0zd 9196 . . . . . . . 8 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → (𝑔𝑦) ∈ ℤ)
15 zdceq 9151 . . . . . . . 8 (((𝑔𝑥) ∈ ℤ ∧ (𝑔𝑦) ∈ ℤ) → DECID (𝑔𝑥) = (𝑔𝑦))
1611, 14, 15syl2anc 409 . . . . . . 7 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → DECID (𝑔𝑥) = (𝑔𝑦))
17 dff1o6 5685 . . . . . . . . . . . . 13 (𝑔:𝐴1-1-onto→ℕ0 ↔ (𝑔 Fn 𝐴 ∧ ran 𝑔 = ℕ0 ∧ ∀𝑥𝐴𝑦𝐴 ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦)))
1817simp3bi 999 . . . . . . . . . . . 12 (𝑔:𝐴1-1-onto→ℕ0 → ∀𝑥𝐴𝑦𝐴 ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦))
1918r19.21bi 2523 . . . . . . . . . . 11 ((𝑔:𝐴1-1-onto→ℕ0𝑥𝐴) → ∀𝑦𝐴 ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦))
2019r19.21bi 2523 . . . . . . . . . 10 (((𝑔:𝐴1-1-onto→ℕ0𝑥𝐴) ∧ 𝑦𝐴) → ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦))
2120anasss 397 . . . . . . . . 9 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦))
22 fveq2 5429 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑔𝑥) = (𝑔𝑦))
2321, 22impbid1 141 . . . . . . . 8 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑔𝑥) = (𝑔𝑦) ↔ 𝑥 = 𝑦))
2423dcbid 824 . . . . . . 7 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → (DECID (𝑔𝑥) = (𝑔𝑦) ↔ DECID 𝑥 = 𝑦))
2516, 24mpbid 146 . . . . . 6 ((𝑔:𝐴1-1-onto→ℕ0 ∧ (𝑥𝐴𝑦𝐴)) → DECID 𝑥 = 𝑦)
2625ralrimivva 2517 . . . . 5 (𝑔:𝐴1-1-onto→ℕ0 → ∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦)
27 f1ocnv 5388 . . . . . . 7 (𝑔:𝐴1-1-onto→ℕ0𝑔:ℕ01-1-onto𝐴)
28 f1ofo 5382 . . . . . . 7 (𝑔:ℕ01-1-onto𝐴𝑔:ℕ0onto𝐴)
2927, 28syl 14 . . . . . 6 (𝑔:𝐴1-1-onto→ℕ0𝑔:ℕ0onto𝐴)
30 peano2nn0 9042 . . . . . . . . 9 (𝑛 ∈ ℕ0 → (𝑛 + 1) ∈ ℕ0)
3130adantl 275 . . . . . . . 8 ((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) → (𝑛 + 1) ∈ ℕ0)
32 elfznn0 9926 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑛) → 𝑗 ∈ ℕ0)
3332adantl 275 . . . . . . . . . . . . . 14 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → 𝑗 ∈ ℕ0)
3433nn0red 9056 . . . . . . . . . . . . 13 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → 𝑗 ∈ ℝ)
35 elfzle2 9840 . . . . . . . . . . . . . . 15 (𝑗 ∈ (0...𝑛) → 𝑗𝑛)
3635adantl 275 . . . . . . . . . . . . . 14 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → 𝑗𝑛)
37 simplr 520 . . . . . . . . . . . . . . 15 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → 𝑛 ∈ ℕ0)
38 nn0leltp1 9142 . . . . . . . . . . . . . . 15 ((𝑗 ∈ ℕ0𝑛 ∈ ℕ0) → (𝑗𝑛𝑗 < (𝑛 + 1)))
3933, 37, 38syl2anc 409 . . . . . . . . . . . . . 14 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → (𝑗𝑛𝑗 < (𝑛 + 1)))
4036, 39mpbid 146 . . . . . . . . . . . . 13 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → 𝑗 < (𝑛 + 1))
4134, 40gtned 7901 . . . . . . . . . . . 12 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → (𝑛 + 1) ≠ 𝑗)
4241neneqd 2330 . . . . . . . . . . 11 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → ¬ (𝑛 + 1) = 𝑗)
43 dff1o6 5685 . . . . . . . . . . . . . . 15 (𝑔:ℕ01-1-onto𝐴 ↔ (𝑔 Fn ℕ0 ∧ ran 𝑔 = 𝐴 ∧ ∀𝑥 ∈ ℕ0𝑦 ∈ ℕ0 ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦)))
4427, 43sylib 121 . . . . . . . . . . . . . 14 (𝑔:𝐴1-1-onto→ℕ0 → (𝑔 Fn ℕ0 ∧ ran 𝑔 = 𝐴 ∧ ∀𝑥 ∈ ℕ0𝑦 ∈ ℕ0 ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦)))
4544simp3d 996 . . . . . . . . . . . . 13 (𝑔:𝐴1-1-onto→ℕ0 → ∀𝑥 ∈ ℕ0𝑦 ∈ ℕ0 ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦))
4645ad2antrr 480 . . . . . . . . . . . 12 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → ∀𝑥 ∈ ℕ0𝑦 ∈ ℕ0 ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦))
4731adantr 274 . . . . . . . . . . . . 13 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → (𝑛 + 1) ∈ ℕ0)
48 fveqeq2 5438 . . . . . . . . . . . . . . 15 (𝑥 = (𝑛 + 1) → ((𝑔𝑥) = (𝑔𝑦) ↔ (𝑔‘(𝑛 + 1)) = (𝑔𝑦)))
49 eqeq1 2147 . . . . . . . . . . . . . . 15 (𝑥 = (𝑛 + 1) → (𝑥 = 𝑦 ↔ (𝑛 + 1) = 𝑦))
5048, 49imbi12d 233 . . . . . . . . . . . . . 14 (𝑥 = (𝑛 + 1) → (((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦) ↔ ((𝑔‘(𝑛 + 1)) = (𝑔𝑦) → (𝑛 + 1) = 𝑦)))
51 fveq2 5429 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑗 → (𝑔𝑦) = (𝑔𝑗))
5251eqeq2d 2152 . . . . . . . . . . . . . . 15 (𝑦 = 𝑗 → ((𝑔‘(𝑛 + 1)) = (𝑔𝑦) ↔ (𝑔‘(𝑛 + 1)) = (𝑔𝑗)))
53 eqeq2 2150 . . . . . . . . . . . . . . 15 (𝑦 = 𝑗 → ((𝑛 + 1) = 𝑦 ↔ (𝑛 + 1) = 𝑗))
5452, 53imbi12d 233 . . . . . . . . . . . . . 14 (𝑦 = 𝑗 → (((𝑔‘(𝑛 + 1)) = (𝑔𝑦) → (𝑛 + 1) = 𝑦) ↔ ((𝑔‘(𝑛 + 1)) = (𝑔𝑗) → (𝑛 + 1) = 𝑗)))
5550, 54rspc2v 2806 . . . . . . . . . . . . 13 (((𝑛 + 1) ∈ ℕ0𝑗 ∈ ℕ0) → (∀𝑥 ∈ ℕ0𝑦 ∈ ℕ0 ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦) → ((𝑔‘(𝑛 + 1)) = (𝑔𝑗) → (𝑛 + 1) = 𝑗)))
5647, 33, 55syl2anc 409 . . . . . . . . . . . 12 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → (∀𝑥 ∈ ℕ0𝑦 ∈ ℕ0 ((𝑔𝑥) = (𝑔𝑦) → 𝑥 = 𝑦) → ((𝑔‘(𝑛 + 1)) = (𝑔𝑗) → (𝑛 + 1) = 𝑗)))
5746, 56mpd 13 . . . . . . . . . . 11 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → ((𝑔‘(𝑛 + 1)) = (𝑔𝑗) → (𝑛 + 1) = 𝑗))
5842, 57mtod 653 . . . . . . . . . 10 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → ¬ (𝑔‘(𝑛 + 1)) = (𝑔𝑗))
5958neqned 2316 . . . . . . . . 9 (((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) ∧ 𝑗 ∈ (0...𝑛)) → (𝑔‘(𝑛 + 1)) ≠ (𝑔𝑗))
6059ralrimiva 2508 . . . . . . . 8 ((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) → ∀𝑗 ∈ (0...𝑛)(𝑔‘(𝑛 + 1)) ≠ (𝑔𝑗))
61 fveq2 5429 . . . . . . . . . . 11 (𝑘 = (𝑛 + 1) → (𝑔𝑘) = (𝑔‘(𝑛 + 1)))
6261neeq1d 2327 . . . . . . . . . 10 (𝑘 = (𝑛 + 1) → ((𝑔𝑘) ≠ (𝑔𝑗) ↔ (𝑔‘(𝑛 + 1)) ≠ (𝑔𝑗)))
6362ralbidv 2438 . . . . . . . . 9 (𝑘 = (𝑛 + 1) → (∀𝑗 ∈ (0...𝑛)(𝑔𝑘) ≠ (𝑔𝑗) ↔ ∀𝑗 ∈ (0...𝑛)(𝑔‘(𝑛 + 1)) ≠ (𝑔𝑗)))
6463rspcev 2793 . . . . . . . 8 (((𝑛 + 1) ∈ ℕ0 ∧ ∀𝑗 ∈ (0...𝑛)(𝑔‘(𝑛 + 1)) ≠ (𝑔𝑗)) → ∃𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑔𝑘) ≠ (𝑔𝑗))
6531, 60, 64syl2anc 409 . . . . . . 7 ((𝑔:𝐴1-1-onto→ℕ0𝑛 ∈ ℕ0) → ∃𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑔𝑘) ≠ (𝑔𝑗))
6665ralrimiva 2508 . . . . . 6 (𝑔:𝐴1-1-onto→ℕ0 → ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑔𝑘) ≠ (𝑔𝑗))
67 cnvexg 5084 . . . . . . . 8 (𝑔 ∈ V → 𝑔 ∈ V)
6867elv 2693 . . . . . . 7 𝑔 ∈ V
69 foeq1 5349 . . . . . . . 8 (𝑓 = 𝑔 → (𝑓:ℕ0onto𝐴𝑔:ℕ0onto𝐴))
70 fveq1 5428 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑓𝑘) = (𝑔𝑘))
71 fveq1 5428 . . . . . . . . . . 11 (𝑓 = 𝑔 → (𝑓𝑗) = (𝑔𝑗))
7270, 71neeq12d 2329 . . . . . . . . . 10 (𝑓 = 𝑔 → ((𝑓𝑘) ≠ (𝑓𝑗) ↔ (𝑔𝑘) ≠ (𝑔𝑗)))
7372rexralbidv 2464 . . . . . . . . 9 (𝑓 = 𝑔 → (∃𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗) ↔ ∃𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑔𝑘) ≠ (𝑔𝑗)))
7473ralbidv 2438 . . . . . . . 8 (𝑓 = 𝑔 → (∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗) ↔ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑔𝑘) ≠ (𝑔𝑗)))
7569, 74anbi12d 465 . . . . . . 7 (𝑓 = 𝑔 → ((𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗)) ↔ (𝑔:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑔𝑘) ≠ (𝑔𝑗))))
7668, 75spcev 2784 . . . . . 6 ((𝑔:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑔𝑘) ≠ (𝑔𝑗)) → ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗)))
7729, 66, 76syl2anc 409 . . . . 5 (𝑔:𝐴1-1-onto→ℕ0 → ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗)))
7826, 77jca 304 . . . 4 (𝑔:𝐴1-1-onto→ℕ0 → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗))))
7978adantl 275 . . 3 ((𝐴 ≈ ℕ0𝑔:𝐴1-1-onto→ℕ0) → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗))))
806, 79exlimddv 1871 . 2 (𝐴 ≈ ℕ0 → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗))))
814, 80syl 14 1 (𝐴 ≈ ℕ → (∀𝑥𝐴𝑦𝐴 DECID 𝑥 = 𝑦 ∧ ∃𝑓(𝑓:ℕ0onto𝐴 ∧ ∀𝑛 ∈ ℕ0𝑘 ∈ ℕ0𝑗 ∈ (0...𝑛)(𝑓𝑘) ≠ (𝑓𝑗))))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  DECID wdc 820   ∧ w3a 963   = wceq 1332  ∃wex 1469   ∈ wcel 1481   ≠ wne 2309  ∀wral 2417  ∃wrex 2418  Vcvv 2689   class class class wbr 3937  ◡ccnv 4546  ran crn 4548   Fn wfn 5126  ⟶wf 5127  –onto→wfo 5129  –1-1-onto→wf1o 5130  ‘cfv 5131  (class class class)co 5782   ≈ cen 6640  0cc0 7645  1c1 7646   + caddc 7648   < clt 7825   ≤ cle 7826  ℕcn 8745  ℕ0cn0 9002  ℤcz 9079  ...cfz 9822 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-cnex 7736  ax-resscn 7737  ax-1cn 7738  ax-1re 7739  ax-icn 7740  ax-addcl 7741  ax-addrcl 7742  ax-mulcl 7743  ax-addcom 7745  ax-addass 7747  ax-distr 7749  ax-i2m1 7750  ax-0lt1 7751  ax-0id 7753  ax-rnegex 7754  ax-cnre 7756  ax-pre-ltirr 7757  ax-pre-ltwlin 7758  ax-pre-lttrn 7759  ax-pre-ltadd 7761 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2914  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-br 3938  df-opab 3998  df-mpt 3999  df-id 4223  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-rn 4558  df-res 4559  df-ima 4560  df-iota 5096  df-fun 5133  df-fn 5134  df-f 5135  df-f1 5136  df-fo 5137  df-f1o 5138  df-fv 5139  df-riota 5738  df-ov 5785  df-oprab 5786  df-mpo 5787  df-er 6437  df-en 6643  df-pnf 7827  df-mnf 7828  df-xr 7829  df-ltxr 7830  df-le 7831  df-sub 7960  df-neg 7961  df-inn 8746  df-n0 9003  df-z 9080  df-uz 9352  df-fz 9823 This theorem is referenced by:  ennnfone  11975
 Copyright terms: Public domain W3C validator