Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  erdszelem8 Structured version   Visualization version   GIF version

Theorem erdszelem8 34020
Description: Lemma for erdsze 34024. (Contributed by Mario Carneiro, 22-Jan-2015.)
Hypotheses
Ref Expression
erdsze.n (𝜑𝑁 ∈ ℕ)
erdsze.f (𝜑𝐹:(1...𝑁)–1-1→ℝ)
erdszelem.k 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝑥𝑦)}), ℝ, < ))
erdszelem.o 𝑂 Or ℝ
erdszelem.a (𝜑𝐴 ∈ (1...𝑁))
erdszelem.b (𝜑𝐵 ∈ (1...𝑁))
erdszelem.l (𝜑𝐴 < 𝐵)
Assertion
Ref Expression
erdszelem8 (𝜑 → ((𝐾𝐴) = (𝐾𝐵) → ¬ (𝐹𝐴)𝑂(𝐹𝐵)))
Distinct variable groups:   𝑥,𝑦,𝐵   𝑥,𝐹,𝑦   𝑥,𝐴,𝑦   𝑥,𝑂,𝑦   𝑥,𝑁,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝐾(𝑥,𝑦)

Proof of Theorem erdszelem8
Dummy variables 𝑤 𝑓 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hashf 14280 . . . . 5 ♯:V⟶(ℕ0 ∪ {+∞})
2 ffun 6707 . . . . 5 (♯:V⟶(ℕ0 ∪ {+∞}) → Fun ♯)
31, 2ax-mp 5 . . . 4 Fun ♯
4 erdszelem.a . . . . 5 (𝜑𝐴 ∈ (1...𝑁))
5 erdsze.n . . . . . 6 (𝜑𝑁 ∈ ℕ)
6 erdsze.f . . . . . 6 (𝜑𝐹:(1...𝑁)–1-1→ℝ)
7 erdszelem.k . . . . . 6 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝑥𝑦)}), ℝ, < ))
8 erdszelem.o . . . . . 6 𝑂 Or ℝ
95, 6, 7, 8erdszelem5 34017 . . . . 5 ((𝜑𝐴 ∈ (1...𝑁)) → (𝐾𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}))
104, 9mpdan 685 . . . 4 (𝜑 → (𝐾𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}))
11 fvelima 6944 . . . 4 ((Fun ♯ ∧ (𝐾𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)})) → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (♯‘𝑓) = (𝐾𝐴))
123, 10, 11sylancr 587 . . 3 (𝜑 → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (♯‘𝑓) = (𝐾𝐴))
13 eqid 2731 . . . . . 6 {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}
1413erdszelem1 34013 . . . . 5 (𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} ↔ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓))
15 fzfid 13920 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ∈ Fin)
16 simplr1 1215 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝐴))
17 ssfi 9156 . . . . . . . . . . 11 (((1...𝐴) ∈ Fin ∧ 𝑓 ⊆ (1...𝐴)) → 𝑓 ∈ Fin)
1815, 16, 17syl2anc 584 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ∈ Fin)
19 hashcl 14298 . . . . . . . . . 10 (𝑓 ∈ Fin → (♯‘𝑓) ∈ ℕ0)
2018, 19syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) ∈ ℕ0)
2120nn0red 12515 . . . . . . . 8 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) ∈ ℝ)
22 eqid 2731 . . . . . . . . . . . . . . 15 {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} = {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}
2322erdszelem2 34014 . . . . . . . . . . . . . 14 ((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℕ)
2423simpri 486 . . . . . . . . . . . . 13 (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℕ
25 nnssre 12198 . . . . . . . . . . . . 13 ℕ ⊆ ℝ
2624, 25sstri 3987 . . . . . . . . . . . 12 (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ
2726a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ)
284elfzelzd 13484 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℤ)
29 erdszelem.b . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (1...𝑁))
3029elfzelzd 13484 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℤ)
31 elfznn 13512 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ)
324, 31syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ ℕ)
3332nnred 12209 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
34 elfznn 13512 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℕ)
3529, 34syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℕ)
3635nnred 12209 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℝ)
37 erdszelem.l . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 < 𝐵)
3833, 36, 37ltled 11344 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴𝐵)
39 eluz2 12810 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (ℤ𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴𝐵))
4028, 30, 38, 39syl3anbrc 1343 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ (ℤ𝐴))
41 fzss2 13523 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ (ℤ𝐴) → (1...𝐴) ⊆ (1...𝐵))
4240, 41syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝐴) ⊆ (1...𝐵))
4342ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ⊆ (1...𝐵))
4416, 43sstrd 3988 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝐵))
45 elfz1end 13513 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵))
4635, 45sylib 217 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ (1...𝐵))
4746ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (1...𝐵))
4847snssd 4805 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → {𝐵} ⊆ (1...𝐵))
4944, 48unssd 4182 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝐵))
50 simplr2 1216 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)))
51 f1f 6774 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ)
526, 51syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:(1...𝑁)⟶ℝ)
5352ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐹:(1...𝑁)⟶ℝ)
54 elfzuz3 13480 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ𝐴))
55 fzss2 13523 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ𝐴) → (1...𝐴) ⊆ (1...𝑁))
564, 54, 553syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝐴) ⊆ (1...𝑁))
5756ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ⊆ (1...𝑁))
5816, 57sstrd 3988 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝑁))
59 fzssuz 13524 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑁) ⊆ (ℤ‘1)
60 uzssz 12825 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℤ‘1) ⊆ ℤ
61 zssre 12547 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℤ ⊆ ℝ
6260, 61sstri 3987 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℤ‘1) ⊆ ℝ
6359, 62sstri 3987 . . . . . . . . . . . . . . . . . . . . . . 23 (1...𝑁) ⊆ ℝ
64 ltso 11276 . . . . . . . . . . . . . . . . . . . . . . 23 < Or ℝ
65 soss 5601 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (1...𝑁)))
6663, 64, 65mp2 9 . . . . . . . . . . . . . . . . . . . . . 22 < Or (1...𝑁)
67 soisores 7308 . . . . . . . . . . . . . . . . . . . . . 22 ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁))) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
6866, 8, 67mpanl12 700 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁)) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
6953, 58, 68syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
7050, 69mpbid 231 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
7170r19.21bi 3247 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
7216sselda 3978 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ (1...𝐴))
73 elfzle2 13487 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ (1...𝐴) → 𝑧𝐴)
7472, 73syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧𝐴)
7558sselda 3978 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ (1...𝑁))
7663, 75sselid 3976 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ ℝ)
774ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ (1...𝑁))
7877, 31syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ ℕ)
7978nnred 12209 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ ℝ)
8076, 79lenltd 11342 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑧𝐴 ↔ ¬ 𝐴 < 𝑧))
8174, 80mpbid 231 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ¬ 𝐴 < 𝑧)
8250adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)))
83 simplr3 1217 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐴𝑓)
8483adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴𝑓)
85 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧𝑓)
86 isorel 7307 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (𝐴 < 𝑧 ↔ ((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧)))
87 fvres 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴𝑓 → ((𝐹𝑓)‘𝐴) = (𝐹𝐴))
88 fvres 6897 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧𝑓 → ((𝐹𝑓)‘𝑧) = (𝐹𝑧))
8987, 88breqan12d 5157 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴𝑓𝑧𝑓) → (((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧) ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
9089adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧) ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
9186, 90bitrd 278 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (𝐴 < 𝑧 ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
9282, 84, 85, 91syl12anc 835 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐴 < 𝑧 ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
9381, 92mtbid 323 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ¬ (𝐹𝐴)𝑂(𝐹𝑧))
94 simplr 767 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐴)𝑂(𝐹𝐵))
9553adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐹:(1...𝑁)⟶ℝ)
9695, 75ffvelcdmd 7072 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑧) ∈ ℝ)
9795, 77ffvelcdmd 7072 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐴) ∈ ℝ)
9829ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (1...𝑁))
9998adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐵 ∈ (1...𝑁))
10095, 99ffvelcdmd 7072 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐵) ∈ ℝ)
101 sotr2 5613 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂 Or ℝ ∧ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ)) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
1028, 101mpan 688 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹𝑧) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
10396, 97, 100, 102syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
10493, 94, 103mp2and 697 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑧)𝑂(𝐹𝐵))
105104a1d 25 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝐵)))
106 elsni 4639 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ {𝐵} → 𝑤 = 𝐵)
107106fveq2d 6882 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ {𝐵} → (𝐹𝑤) = (𝐹𝐵))
108107breq2d 5153 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ {𝐵} → ((𝐹𝑧)𝑂(𝐹𝑤) ↔ (𝐹𝑧)𝑂(𝐹𝐵)))
109108imbi2d 340 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝐵))))
110105, 109syl5ibrcom 246 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑤 ∈ {𝐵} → (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
111110ralrimiv 3144 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
112 ralunb 4187 . . . . . . . . . . . . . . . . . 18 (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (∀𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ∧ ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
11371, 111, 112sylanbrc 583 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
114113ralrimiva 3145 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧𝑓𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
11549sselda 3978 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → 𝑤 ∈ (1...𝐵))
116 elfzle2 13487 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ (1...𝐵) → 𝑤𝐵)
117116adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤𝐵)
118 elfzelz 13483 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℤ)
119118zred 12648 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℝ)
120119adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ∈ ℝ)
12136ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝐵 ∈ ℝ)
122120, 121lenltd 11342 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → (𝑤𝐵 ↔ ¬ 𝐵 < 𝑤))
123117, 122mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → ¬ 𝐵 < 𝑤)
124115, 123syldan 591 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → ¬ 𝐵 < 𝑤)
125124pm2.21d 121 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → (𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
126125ralrimiva 3145 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
127 elsni 4639 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
128127breq1d 5151 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝐵} → (𝑧 < 𝑤𝐵 < 𝑤))
129128imbi1d 341 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
130129ralbidv 3176 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝐵} → (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
131126, 130syl5ibrcom 246 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑧 ∈ {𝐵} → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
132131ralrimiv 3144 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
133 ralunb 4187 . . . . . . . . . . . . . . . 16 (∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (∀𝑧𝑓𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ∧ ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
134114, 132, 133sylanbrc 583 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
13598snssd 4805 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → {𝐵} ⊆ (1...𝑁))
13658, 135unssd 4182 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))
137 soisores 7308 . . . . . . . . . . . . . . . . 17 ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
13866, 8, 137mpanl12 700 . . . . . . . . . . . . . . . 16 ((𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
13953, 136, 138syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
140134, 139mpbird 256 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))))
141 ssun2 4169 . . . . . . . . . . . . . . 15 {𝐵} ⊆ (𝑓 ∪ {𝐵})
142 snssg 4780 . . . . . . . . . . . . . . . 16 (𝐵 ∈ (1...𝐵) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
14347, 142syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
144141, 143mpbiri 257 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (𝑓 ∪ {𝐵}))
14522erdszelem1 34013 . . . . . . . . . . . . . 14 ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} ↔ ((𝑓 ∪ {𝐵}) ⊆ (1...𝐵) ∧ (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ∧ 𝐵 ∈ (𝑓 ∪ {𝐵})))
14649, 140, 144, 145syl3anbrc 1343 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})
147 vex 3477 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
148 snex 5424 . . . . . . . . . . . . . . . 16 {𝐵} ∈ V
149147, 148unex 7716 . . . . . . . . . . . . . . 15 (𝑓 ∪ {𝐵}) ∈ V
1501fdmi 6716 . . . . . . . . . . . . . . 15 dom ♯ = V
151149, 150eleqtrri 2831 . . . . . . . . . . . . . 14 (𝑓 ∪ {𝐵}) ∈ dom ♯
152 funfvima 7216 . . . . . . . . . . . . . 14 ((Fun ♯ ∧ (𝑓 ∪ {𝐵}) ∈ dom ♯) → ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})))
1533, 151, 152mp2an 690 . . . . . . . . . . . . 13 ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
154146, 153syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
155154ne0d 4331 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅)
15623simpli 484 . . . . . . . . . . . 12 (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin
157 fimaxre2 12141 . . . . . . . . . . . 12 (((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧)
15827, 156, 157sylancl 586 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧)
15933, 36ltnled 11343 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
16037, 159mpbid 231 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ 𝐵𝐴)
161 elfzle2 13487 . . . . . . . . . . . . . . . 16 (𝐵 ∈ (1...𝐴) → 𝐵𝐴)
162160, 161nsyl 140 . . . . . . . . . . . . . . 15 (𝜑 → ¬ 𝐵 ∈ (1...𝐴))
163162ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ¬ 𝐵 ∈ (1...𝐴))
16416, 163ssneldd 3981 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ¬ 𝐵𝑓)
165 hashunsng 14334 . . . . . . . . . . . . . 14 (𝐵 ∈ (1...𝑁) → ((𝑓 ∈ Fin ∧ ¬ 𝐵𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
16698, 165syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝑓 ∈ Fin ∧ ¬ 𝐵𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
16718, 164, 166mp2and 697 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1))
168167, 154eqeltrrd 2833 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
169 suprub 12157 . . . . . . . . . . 11 ((((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧) ∧ ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
17027, 155, 158, 168, 169syl31anc 1373 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
1715, 6, 7erdszelem3 34015 . . . . . . . . . . . 12 (𝐵 ∈ (1...𝑁) → (𝐾𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
17229, 171syl 17 . . . . . . . . . . 11 (𝜑 → (𝐾𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
173172ad2antrr 724 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
174170, 173breqtrrd 5169 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) + 1) ≤ (𝐾𝐵))
1755, 6, 7, 8erdszelem6 34018 . . . . . . . . . . . . 13 (𝜑𝐾:(1...𝑁)⟶ℕ)
176175, 29ffvelcdmd 7072 . . . . . . . . . . . 12 (𝜑 → (𝐾𝐵) ∈ ℕ)
177176ad2antrr 724 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) ∈ ℕ)
178177nnnn0d 12514 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) ∈ ℕ0)
179 nn0ltp1le 12602 . . . . . . . . . 10 (((♯‘𝑓) ∈ ℕ0 ∧ (𝐾𝐵) ∈ ℕ0) → ((♯‘𝑓) < (𝐾𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾𝐵)))
18020, 178, 179syl2anc 584 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) < (𝐾𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾𝐵)))
181174, 180mpbird 256 . . . . . . . 8 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) < (𝐾𝐵))
18221, 181ltned 11332 . . . . . . 7 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) ≠ (𝐾𝐵))
183182ex 413 . . . . . 6 ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) → ((𝐹𝐴)𝑂(𝐹𝐵) → (♯‘𝑓) ≠ (𝐾𝐵)))
184 neeq1 3002 . . . . . . 7 ((♯‘𝑓) = (𝐾𝐴) → ((♯‘𝑓) ≠ (𝐾𝐵) ↔ (𝐾𝐴) ≠ (𝐾𝐵)))
185184imbi2d 340 . . . . . 6 ((♯‘𝑓) = (𝐾𝐴) → (((𝐹𝐴)𝑂(𝐹𝐵) → (♯‘𝑓) ≠ (𝐾𝐵)) ↔ ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
186183, 185syl5ibcom 244 . . . . 5 ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) → ((♯‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
18714, 186sylan2b 594 . . . 4 ((𝜑𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}) → ((♯‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
188187rexlimdva 3154 . . 3 (𝜑 → (∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (♯‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
18912, 188mpd 15 . 2 (𝜑 → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵)))
190189necon2bd 2955 1 (𝜑 → ((𝐾𝐴) = (𝐾𝐵) → ¬ (𝐹𝐴)𝑂(𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2939  wral 3060  wrex 3069  {crab 3431  Vcvv 3473  cun 3942  wss 3944  c0 4318  𝒫 cpw 4596  {csn 4622   class class class wbr 5141  cmpt 5224   Or wor 5580  dom cdm 5669  cres 5671  cima 5672  Fun wfun 6526  wf 6528  1-1wf1 6529  cfv 6532   Isom wiso 6533  (class class class)co 7393  Fincfn 8922  supcsup 9417  cr 11091  1c1 11093   + caddc 11095  +∞cpnf 11227   < clt 11230  cle 11231  cn 12194  0cn0 12454  cz 12540  cuz 12804  ...cfz 13466  chash 14272
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 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708  ax-cnex 11148  ax-resscn 11149  ax-1cn 11150  ax-icn 11151  ax-addcl 11152  ax-addrcl 11153  ax-mulcl 11154  ax-mulrcl 11155  ax-mulcom 11156  ax-addass 11157  ax-mulass 11158  ax-distr 11159  ax-i2m1 11160  ax-1ne0 11161  ax-1rid 11162  ax-rnegex 11163  ax-rrecex 11164  ax-cnre 11165  ax-pre-lttri 11166  ax-pre-lttrn 11167  ax-pre-ltadd 11168  ax-pre-mulgt0 11169  ax-pre-sup 11170
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 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-int 4944  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6289  df-ord 6356  df-on 6357  df-lim 6358  df-suc 6359  df-iota 6484  df-fun 6534  df-fn 6535  df-f 6536  df-f1 6537  df-fo 6538  df-f1o 6539  df-fv 6540  df-isom 6541  df-riota 7349  df-ov 7396  df-oprab 7397  df-mpo 7398  df-om 7839  df-1st 7957  df-2nd 7958  df-frecs 8248  df-wrecs 8279  df-recs 8353  df-rdg 8392  df-1o 8448  df-oadd 8452  df-er 8686  df-en 8923  df-dom 8924  df-sdom 8925  df-fin 8926  df-sup 9419  df-dju 9878  df-card 9916  df-pnf 11232  df-mnf 11233  df-xr 11234  df-ltxr 11235  df-le 11236  df-sub 11428  df-neg 11429  df-nn 12195  df-n0 12455  df-xnn0 12527  df-z 12541  df-uz 12805  df-fz 13467  df-hash 14273
This theorem is referenced by:  erdszelem9  34021
  Copyright terms: Public domain W3C validator