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 32723
Description: Lemma for erdsze 32727. (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 13783 . . . . 5 ♯:V⟶(ℕ0 ∪ {+∞})
2 ffun 6501 . . . . 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 32720 . . . . 5 ((𝜑𝐴 ∈ (1...𝑁)) → (𝐾𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}))
104, 9mpdan 687 . . . 4 (𝜑 → (𝐾𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}))
11 fvelima 6729 . . . 4 ((Fun ♯ ∧ (𝐾𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)})) → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (♯‘𝑓) = (𝐾𝐴))
123, 10, 11sylancr 590 . . 3 (𝜑 → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (♯‘𝑓) = (𝐾𝐴))
13 eqid 2738 . . . . . 6 {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}
1413erdszelem1 32716 . . . . 5 (𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} ↔ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓))
15 fzfid 13425 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ∈ Fin)
16 simplr1 1216 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝐴))
17 ssfi 8765 . . . . . . . . . . 11 (((1...𝐴) ∈ Fin ∧ 𝑓 ⊆ (1...𝐴)) → 𝑓 ∈ Fin)
1815, 16, 17syl2anc 587 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ∈ Fin)
19 hashcl 13802 . . . . . . . . . 10 (𝑓 ∈ Fin → (♯‘𝑓) ∈ ℕ0)
2018, 19syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) ∈ ℕ0)
2120nn0red 12030 . . . . . . . 8 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) ∈ ℝ)
22 eqid 2738 . . . . . . . . . . . . . . 15 {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} = {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}
2322erdszelem2 32717 . . . . . . . . . . . . . 14 ((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℕ)
2423simpri 489 . . . . . . . . . . . . 13 (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℕ
25 nnssre 11713 . . . . . . . . . . . . 13 ℕ ⊆ ℝ
2624, 25sstri 3884 . . . . . . . . . . . 12 (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ
2726a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ)
284elfzelzd 12992 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℤ)
29 erdszelem.b . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ (1...𝑁))
3029elfzelzd 12992 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℤ)
31 elfznn 13020 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ)
324, 31syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐴 ∈ ℕ)
3332nnred 11724 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℝ)
34 elfznn 13020 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℕ)
3529, 34syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ ℕ)
3635nnred 11724 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℝ)
37 erdszelem.l . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 < 𝐵)
3833, 36, 37ltled 10859 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴𝐵)
39 eluz2 12323 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (ℤ𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴𝐵))
4028, 30, 38, 39syl3anbrc 1344 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ (ℤ𝐴))
41 fzss2 13031 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ (ℤ𝐴) → (1...𝐴) ⊆ (1...𝐵))
4240, 41syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (1...𝐴) ⊆ (1...𝐵))
4342ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ⊆ (1...𝐵))
4416, 43sstrd 3885 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝐵))
45 elfz1end 13021 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵))
4635, 45sylib 221 . . . . . . . . . . . . . . . . 17 (𝜑𝐵 ∈ (1...𝐵))
4746ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (1...𝐵))
4847snssd 4694 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → {𝐵} ⊆ (1...𝐵))
4944, 48unssd 4074 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝐵))
50 simplr2 1217 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)))
51 f1f 6568 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ)
526, 51syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝐹:(1...𝑁)⟶ℝ)
5352ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐹:(1...𝑁)⟶ℝ)
54 elfzuz3 12988 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ𝐴))
55 fzss2 13031 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ (ℤ𝐴) → (1...𝐴) ⊆ (1...𝑁))
564, 54, 553syl 18 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (1...𝐴) ⊆ (1...𝑁))
5756ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ⊆ (1...𝑁))
5816, 57sstrd 3885 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝑁))
59 fzssuz 13032 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑁) ⊆ (ℤ‘1)
60 uzssz 12338 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℤ‘1) ⊆ ℤ
61 zssre 12062 . . . . . . . . . . . . . . . . . . . . . . . . 25 ℤ ⊆ ℝ
6260, 61sstri 3884 . . . . . . . . . . . . . . . . . . . . . . . 24 (ℤ‘1) ⊆ ℝ
6359, 62sstri 3884 . . . . . . . . . . . . . . . . . . . . . . 23 (1...𝑁) ⊆ ℝ
64 ltso 10792 . . . . . . . . . . . . . . . . . . . . . . 23 < Or ℝ
65 soss 5457 . . . . . . . . . . . . . . . . . . . . . . 23 ((1...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (1...𝑁)))
6663, 64, 65mp2 9 . . . . . . . . . . . . . . . . . . . . . 22 < Or (1...𝑁)
67 soisores 7087 . . . . . . . . . . . . . . . . . . . . . 22 ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁))) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
6866, 8, 67mpanl12 702 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁)) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
6953, 58, 68syl2anc 587 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
7050, 69mpbid 235 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
7170r19.21bi 3120 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
7216sselda 3875 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ (1...𝐴))
73 elfzle2 12995 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ∈ (1...𝐴) → 𝑧𝐴)
7472, 73syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧𝐴)
7558sselda 3875 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ (1...𝑁))
7663, 75sseldi 3873 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ ℝ)
774ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ (1...𝑁))
7877, 31syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ ℕ)
7978nnred 11724 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ ℝ)
8076, 79lenltd 10857 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑧𝐴 ↔ ¬ 𝐴 < 𝑧))
8174, 80mpbid 235 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ¬ 𝐴 < 𝑧)
8250adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)))
83 simplr3 1218 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐴𝑓)
8483adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴𝑓)
85 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧𝑓)
86 isorel 7086 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (𝐴 < 𝑧 ↔ ((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧)))
87 fvres 6687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐴𝑓 → ((𝐹𝑓)‘𝐴) = (𝐹𝐴))
88 fvres 6687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧𝑓 → ((𝐹𝑓)‘𝑧) = (𝐹𝑧))
8987, 88breqan12d 5043 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴𝑓𝑧𝑓) → (((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧) ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
9089adantl 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧) ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
9186, 90bitrd 282 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (𝐴 < 𝑧 ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
9282, 84, 85, 91syl12anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐴 < 𝑧 ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
9381, 92mtbid 327 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ¬ (𝐹𝐴)𝑂(𝐹𝑧))
94 simplr 769 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐴)𝑂(𝐹𝐵))
9553adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐹:(1...𝑁)⟶ℝ)
9695, 75ffvelrnd 6856 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑧) ∈ ℝ)
9795, 77ffvelrnd 6856 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐴) ∈ ℝ)
9829ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (1...𝑁))
9998adantr 484 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐵 ∈ (1...𝑁))
10095, 99ffvelrnd 6856 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐵) ∈ ℝ)
101 sotr2 5469 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑂 Or ℝ ∧ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ)) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
1028, 101mpan 690 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹𝑧) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
10396, 97, 100, 102syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
10493, 94, 103mp2and 699 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑧)𝑂(𝐹𝐵))
105104a1d 25 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝐵)))
106 elsni 4530 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ {𝐵} → 𝑤 = 𝐵)
107106fveq2d 6672 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ {𝐵} → (𝐹𝑤) = (𝐹𝐵))
108107breq2d 5039 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ {𝐵} → ((𝐹𝑧)𝑂(𝐹𝑤) ↔ (𝐹𝑧)𝑂(𝐹𝐵)))
109108imbi2d 344 . . . . . . . . . . . . . . . . . . . 20 (𝑤 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝐵))))
110105, 109syl5ibrcom 250 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑤 ∈ {𝐵} → (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
111110ralrimiv 3095 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
112 ralunb 4079 . . . . . . . . . . . . . . . . . 18 (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (∀𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ∧ ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
11371, 111, 112sylanbrc 586 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
114113ralrimiva 3096 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧𝑓𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
11549sselda 3875 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → 𝑤 ∈ (1...𝐵))
116 elfzle2 12995 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ (1...𝐵) → 𝑤𝐵)
117116adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤𝐵)
118 elfzelz 12991 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℤ)
119118zred 12161 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℝ)
120119adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ∈ ℝ)
12136ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝐵 ∈ ℝ)
122120, 121lenltd 10857 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → (𝑤𝐵 ↔ ¬ 𝐵 < 𝑤))
123117, 122mpbid 235 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → ¬ 𝐵 < 𝑤)
124115, 123syldan 594 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → ¬ 𝐵 < 𝑤)
125124pm2.21d 121 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → (𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
126125ralrimiva 3096 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
127 elsni 4530 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
128127breq1d 5037 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝐵} → (𝑧 < 𝑤𝐵 < 𝑤))
129128imbi1d 345 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
130129ralbidv 3109 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ {𝐵} → (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
131126, 130syl5ibrcom 250 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑧 ∈ {𝐵} → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
132131ralrimiv 3095 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
133 ralunb 4079 . . . . . . . . . . . . . . . 16 (∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (∀𝑧𝑓𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ∧ ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
134114, 132, 133sylanbrc 586 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
13598snssd 4694 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → {𝐵} ⊆ (1...𝑁))
13658, 135unssd 4074 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))
137 soisores 7087 . . . . . . . . . . . . . . . . 17 ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
13866, 8, 137mpanl12 702 . . . . . . . . . . . . . . . 16 ((𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
13953, 136, 138syl2anc 587 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
140134, 139mpbird 260 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))))
141 ssun2 4061 . . . . . . . . . . . . . . 15 {𝐵} ⊆ (𝑓 ∪ {𝐵})
142 snssg 4670 . . . . . . . . . . . . . . . 16 (𝐵 ∈ (1...𝐵) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
14347, 142syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
144141, 143mpbiri 261 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (𝑓 ∪ {𝐵}))
14522erdszelem1 32716 . . . . . . . . . . . . . 14 ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} ↔ ((𝑓 ∪ {𝐵}) ⊆ (1...𝐵) ∧ (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ∧ 𝐵 ∈ (𝑓 ∪ {𝐵})))
14649, 140, 144, 145syl3anbrc 1344 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})
147 vex 3401 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
148 snex 5295 . . . . . . . . . . . . . . . 16 {𝐵} ∈ V
149147, 148unex 7481 . . . . . . . . . . . . . . 15 (𝑓 ∪ {𝐵}) ∈ V
1501fdmi 6510 . . . . . . . . . . . . . . 15 dom ♯ = V
151149, 150eleqtrri 2832 . . . . . . . . . . . . . 14 (𝑓 ∪ {𝐵}) ∈ dom ♯
152 funfvima 6997 . . . . . . . . . . . . . 14 ((Fun ♯ ∧ (𝑓 ∪ {𝐵}) ∈ dom ♯) → ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})))
1533, 151, 152mp2an 692 . . . . . . . . . . . . 13 ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
154146, 153syl 17 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
155154ne0d 4222 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅)
15623simpli 487 . . . . . . . . . . . 12 (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin
157 fimaxre2 11656 . . . . . . . . . . . 12 (((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧)
15827, 156, 157sylancl 589 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧)
15933, 36ltnled 10858 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
16037, 159mpbid 235 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ 𝐵𝐴)
161 elfzle2 12995 . . . . . . . . . . . . . . . 16 (𝐵 ∈ (1...𝐴) → 𝐵𝐴)
162160, 161nsyl 142 . . . . . . . . . . . . . . 15 (𝜑 → ¬ 𝐵 ∈ (1...𝐴))
163162ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ¬ 𝐵 ∈ (1...𝐴))
16416, 163ssneldd 3878 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ¬ 𝐵𝑓)
165 hashunsng 13838 . . . . . . . . . . . . . 14 (𝐵 ∈ (1...𝑁) → ((𝑓 ∈ Fin ∧ ¬ 𝐵𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
16698, 165syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝑓 ∈ Fin ∧ ¬ 𝐵𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
16718, 164, 166mp2and 699 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1))
168167, 154eqeltrrd 2834 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
169 suprub 11672 . . . . . . . . . . 11 ((((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧) ∧ ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
17027, 155, 158, 168, 169syl31anc 1374 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
1715, 6, 7erdszelem3 32718 . . . . . . . . . . . 12 (𝐵 ∈ (1...𝑁) → (𝐾𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
17229, 171syl 17 . . . . . . . . . . 11 (𝜑 → (𝐾𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
173172ad2antrr 726 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
174170, 173breqtrrd 5055 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) + 1) ≤ (𝐾𝐵))
1755, 6, 7, 8erdszelem6 32721 . . . . . . . . . . . . 13 (𝜑𝐾:(1...𝑁)⟶ℕ)
176175, 29ffvelrnd 6856 . . . . . . . . . . . 12 (𝜑 → (𝐾𝐵) ∈ ℕ)
177176ad2antrr 726 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) ∈ ℕ)
178177nnnn0d 12029 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) ∈ ℕ0)
179 nn0ltp1le 12114 . . . . . . . . . 10 (((♯‘𝑓) ∈ ℕ0 ∧ (𝐾𝐵) ∈ ℕ0) → ((♯‘𝑓) < (𝐾𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾𝐵)))
18020, 178, 179syl2anc 587 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) < (𝐾𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾𝐵)))
181174, 180mpbird 260 . . . . . . . 8 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) < (𝐾𝐵))
18221, 181ltned 10847 . . . . . . 7 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) ≠ (𝐾𝐵))
183182ex 416 . . . . . 6 ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) → ((𝐹𝐴)𝑂(𝐹𝐵) → (♯‘𝑓) ≠ (𝐾𝐵)))
184 neeq1 2996 . . . . . . 7 ((♯‘𝑓) = (𝐾𝐴) → ((♯‘𝑓) ≠ (𝐾𝐵) ↔ (𝐾𝐴) ≠ (𝐾𝐵)))
185184imbi2d 344 . . . . . 6 ((♯‘𝑓) = (𝐾𝐴) → (((𝐹𝐴)𝑂(𝐹𝐵) → (♯‘𝑓) ≠ (𝐾𝐵)) ↔ ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
186183, 185syl5ibcom 248 . . . . 5 ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) → ((♯‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
18714, 186sylan2b 597 . . . 4 ((𝜑𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}) → ((♯‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
188187rexlimdva 3193 . . 3 (𝜑 → (∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (♯‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
18912, 188mpd 15 . 2 (𝜑 → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵)))
190189necon2bd 2950 1 (𝜑 → ((𝐾𝐴) = (𝐾𝐵) → ¬ (𝐹𝐴)𝑂(𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1088   = wceq 1542  wcel 2113  wne 2934  wral 3053  wrex 3054  {crab 3057  Vcvv 3397  cun 3839  wss 3841  c0 4209  𝒫 cpw 4485  {csn 4513   class class class wbr 5027  cmpt 5107   Or wor 5437  dom cdm 5519  cres 5521  cima 5522  Fun wfun 6327  wf 6329  1-1wf1 6330  cfv 6333   Isom wiso 6334  (class class class)co 7164  Fincfn 8548  supcsup 8970  cr 10607  1c1 10609   + caddc 10611  +∞cpnf 10743   < clt 10746  cle 10747  cn 11709  0cn0 11969  cz 12055  cuz 12317  ...cfz 12974  chash 13775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-cnex 10664  ax-resscn 10665  ax-1cn 10666  ax-icn 10667  ax-addcl 10668  ax-addrcl 10669  ax-mulcl 10670  ax-mulrcl 10671  ax-mulcom 10672  ax-addass 10673  ax-mulass 10674  ax-distr 10675  ax-i2m1 10676  ax-1ne0 10677  ax-1rid 10678  ax-rnegex 10679  ax-rrecex 10680  ax-cnre 10681  ax-pre-lttri 10682  ax-pre-lttrn 10683  ax-pre-ltadd 10684  ax-pre-mulgt0 10685  ax-pre-sup 10686
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-int 4834  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6123  df-ord 6169  df-on 6170  df-lim 6171  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-isom 6342  df-riota 7121  df-ov 7167  df-oprab 7168  df-mpo 7169  df-om 7594  df-1st 7707  df-2nd 7708  df-wrecs 7969  df-recs 8030  df-rdg 8068  df-1o 8124  df-oadd 8128  df-er 8313  df-en 8549  df-dom 8550  df-sdom 8551  df-fin 8552  df-sup 8972  df-dju 9396  df-card 9434  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752  df-sub 10943  df-neg 10944  df-nn 11710  df-n0 11970  df-xnn0 12042  df-z 12056  df-uz 12318  df-fz 12975  df-hash 13776
This theorem is referenced by:  erdszelem9  32724
  Copyright terms: Public domain W3C validator