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 30923
Description: Lemma for erdsze 30927. (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 13073 . . . . 5 #:V⟶(ℕ0 ∪ {+∞})
2 ffun 6010 . . . . 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 30920 . . . . 5 ((𝜑𝐴 ∈ (1...𝑁)) → (𝐾𝐴) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}))
104, 9mpdan 701 . . . 4 (𝜑 → (𝐾𝐴) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}))
11 fvelima 6210 . . . 4 ((Fun # ∧ (𝐾𝐴) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)})) → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (#‘𝑓) = (𝐾𝐴))
123, 10, 11sylancr 694 . . 3 (𝜑 → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (#‘𝑓) = (𝐾𝐴))
13 eqid 2621 . . . . . 6 {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}
1413erdszelem1 30916 . . . . 5 (𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} ↔ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓))
15 fzfid 12720 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ∈ Fin)
16 simplr1 1101 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝐴))
17 ssfi 8132 . . . . . . . . . . 11 (((1...𝐴) ∈ Fin ∧ 𝑓 ⊆ (1...𝐴)) → 𝑓 ∈ Fin)
1815, 16, 17syl2anc 692 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ∈ Fin)
19 hashcl 13095 . . . . . . . . . 10 (𝑓 ∈ Fin → (#‘𝑓) ∈ ℕ0)
2018, 19syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘𝑓) ∈ ℕ0)
2120nn0red 11304 . . . . . . . 8 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘𝑓) ∈ ℝ)
22 eqid 2621 . . . . . . . . . . . . . . 15 {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} = {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}
2322erdszelem2 30917 . . . . . . . . . . . . . 14 ((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin ∧ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℕ)
2423simpri 478 . . . . . . . . . . . . 13 (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℕ
25 nnssre 10976 . . . . . . . . . . . . 13 ℕ ⊆ ℝ
2624, 25sstri 3596 . . . . . . . . . . . 12 (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ
2726a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ)
28 erdszelem.l . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 < 𝐵)
29 elfznn 12320 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ)
304, 29syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℕ)
3130nnred 10987 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
32 erdszelem.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ (1...𝑁))
33 elfznn 12320 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℕ)
3432, 33syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℕ)
3534nnred 10987 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ)
3631, 35ltnled 10136 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
3728, 36mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ 𝐵𝐴)
38 elfzle2 12295 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (1...𝐴) → 𝐵𝐴)
3937, 38nsyl 135 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ 𝐵 ∈ (1...𝐴))
4039ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ¬ 𝐵 ∈ (1...𝐴))
4116, 40ssneldd 3590 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ¬ 𝐵𝑓)
4232ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (1...𝑁))
43 hashunsng 13129 . . . . . . . . . . . . . . 15 (𝐵 ∈ (1...𝑁) → ((𝑓 ∈ Fin ∧ ¬ 𝐵𝑓) → (#‘(𝑓 ∪ {𝐵})) = ((#‘𝑓) + 1)))
4442, 43syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝑓 ∈ Fin ∧ ¬ 𝐵𝑓) → (#‘(𝑓 ∪ {𝐵})) = ((#‘𝑓) + 1)))
4518, 41, 44mp2and 714 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘(𝑓 ∪ {𝐵})) = ((#‘𝑓) + 1))
46 elfzelz 12292 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℤ)
474, 46syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℤ)
48 elfzelz 12292 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℤ)
4932, 48syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℤ)
5031, 35, 28ltled 10137 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴𝐵)
51 eluz2 11645 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ (ℤ𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴𝐵))
5247, 49, 50, 51syl3anbrc 1244 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ (ℤ𝐴))
53 fzss2 12331 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (ℤ𝐴) → (1...𝐴) ⊆ (1...𝐵))
5452, 53syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...𝐴) ⊆ (1...𝐵))
5554ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ⊆ (1...𝐵))
5616, 55sstrd 3597 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝐵))
57 elfz1end 12321 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵))
5834, 57sylib 208 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ (1...𝐵))
5958ad2antrr 761 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (1...𝐵))
6059snssd 4314 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → {𝐵} ⊆ (1...𝐵))
6156, 60unssd 3772 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝐵))
62 simplr2 1102 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)))
63 f1f 6063 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ)
646, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹:(1...𝑁)⟶ℝ)
6564ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐹:(1...𝑁)⟶ℝ)
66 elfzuz3 12289 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ𝐴))
67 fzss2 12331 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ𝐴) → (1...𝐴) ⊆ (1...𝑁))
684, 66, 673syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...𝐴) ⊆ (1...𝑁))
6968ad2antrr 761 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ⊆ (1...𝑁))
7016, 69sstrd 3597 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝑁))
71 fzssuz 12332 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...𝑁) ⊆ (ℤ‘1)
72 uzssz 11659 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ℤ‘1) ⊆ ℤ
73 zssre 11336 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℤ ⊆ ℝ
7472, 73sstri 3596 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℤ‘1) ⊆ ℝ
7571, 74sstri 3596 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑁) ⊆ ℝ
76 ltso 10070 . . . . . . . . . . . . . . . . . . . . . . . 24 < Or ℝ
77 soss 5018 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (1...𝑁)))
7875, 76, 77mp2 9 . . . . . . . . . . . . . . . . . . . . . . 23 < Or (1...𝑁)
79 soisores 6537 . . . . . . . . . . . . . . . . . . . . . . 23 ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁))) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
8078, 8, 79mpanl12 717 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁)) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
8165, 70, 80syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
8262, 81mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
8382r19.21bi 2927 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
8416sselda 3587 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ (1...𝐴))
85 elfzle2 12295 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ (1...𝐴) → 𝑧𝐴)
8684, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧𝐴)
8770sselda 3587 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ (1...𝑁))
8875, 87sseldi 3585 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ ℝ)
894ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ (1...𝑁))
9089, 29syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ ℕ)
9190nnred 10987 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ ℝ)
9288, 91lenltd 10135 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑧𝐴 ↔ ¬ 𝐴 < 𝑧))
9386, 92mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ¬ 𝐴 < 𝑧)
9462adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)))
95 simplr3 1103 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐴𝑓)
9695adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴𝑓)
97 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧𝑓)
98 isorel 6536 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (𝐴 < 𝑧 ↔ ((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧)))
99 fvres 6169 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴𝑓 → ((𝐹𝑓)‘𝐴) = (𝐹𝐴))
100 fvres 6169 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧𝑓 → ((𝐹𝑓)‘𝑧) = (𝐹𝑧))
10199, 100breqan12d 4634 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴𝑓𝑧𝑓) → (((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧) ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
102101adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧) ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
10398, 102bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (𝐴 < 𝑧 ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
10494, 96, 97, 103syl12anc 1321 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐴 < 𝑧 ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
10593, 104mtbid 314 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ¬ (𝐹𝐴)𝑂(𝐹𝑧))
106 simplr 791 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐴)𝑂(𝐹𝐵))
10765adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐹:(1...𝑁)⟶ℝ)
108107, 87ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑧) ∈ ℝ)
109107, 89ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐴) ∈ ℝ)
11042adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐵 ∈ (1...𝑁))
111107, 110ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐵) ∈ ℝ)
112 sotr2 5029 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 Or ℝ ∧ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ)) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
1138, 112mpan 705 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑧) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
114108, 109, 111, 113syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
115105, 106, 114mp2and 714 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑧)𝑂(𝐹𝐵))
116115a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝐵)))
117 elsni 4170 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ {𝐵} → 𝑤 = 𝐵)
118117fveq2d 6157 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ {𝐵} → (𝐹𝑤) = (𝐹𝐵))
119118breq2d 4630 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ {𝐵} → ((𝐹𝑧)𝑂(𝐹𝑤) ↔ (𝐹𝑧)𝑂(𝐹𝐵)))
120119imbi2d 330 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝐵))))
121116, 120syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑤 ∈ {𝐵} → (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
122121ralrimiv 2960 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
123 ralunb 3777 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (∀𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ∧ ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
12483, 122, 123sylanbrc 697 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
125124ralrimiva 2961 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧𝑓𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
12661sselda 3587 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → 𝑤 ∈ (1...𝐵))
127 elfzle2 12295 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ (1...𝐵) → 𝑤𝐵)
128127adantl 482 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤𝐵)
129 elfzelz 12292 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℤ)
130129zred 11434 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℝ)
131130adantl 482 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ∈ ℝ)
13235ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝐵 ∈ ℝ)
133131, 132lenltd 10135 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → (𝑤𝐵 ↔ ¬ 𝐵 < 𝑤))
134128, 133mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → ¬ 𝐵 < 𝑤)
135126, 134syldan 487 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → ¬ 𝐵 < 𝑤)
136135pm2.21d 118 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → (𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
137136ralrimiva 2961 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
138 elsni 4170 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
139138breq1d 4628 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ {𝐵} → (𝑧 < 𝑤𝐵 < 𝑤))
140139imbi1d 331 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
141140ralbidv 2981 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ {𝐵} → (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
142137, 141syl5ibrcom 237 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑧 ∈ {𝐵} → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
143142ralrimiv 2960 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
144 ralunb 3777 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (∀𝑧𝑓𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ∧ ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
145125, 143, 144sylanbrc 697 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
14642snssd 4314 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → {𝐵} ⊆ (1...𝑁))
14770, 146unssd 3772 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))
148 soisores 6537 . . . . . . . . . . . . . . . . . 18 ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
14978, 8, 148mpanl12 717 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
15065, 147, 149syl2anc 692 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
151145, 150mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))))
152 ssun2 3760 . . . . . . . . . . . . . . . 16 {𝐵} ⊆ (𝑓 ∪ {𝐵})
153 snssg 4301 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (1...𝐵) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
15459, 153syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
155152, 154mpbiri 248 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (𝑓 ∪ {𝐵}))
15622erdszelem1 30916 . . . . . . . . . . . . . . 15 ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} ↔ ((𝑓 ∪ {𝐵}) ⊆ (1...𝐵) ∧ (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ∧ 𝐵 ∈ (𝑓 ∪ {𝐵})))
15761, 151, 155, 156syl3anbrc 1244 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})
158 vex 3192 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
159 snex 4874 . . . . . . . . . . . . . . . . 17 {𝐵} ∈ V
160158, 159unex 6916 . . . . . . . . . . . . . . . 16 (𝑓 ∪ {𝐵}) ∈ V
1611fdmi 6014 . . . . . . . . . . . . . . . 16 dom # = V
162160, 161eleqtrri 2697 . . . . . . . . . . . . . . 15 (𝑓 ∪ {𝐵}) ∈ dom #
163 funfvima 6452 . . . . . . . . . . . . . . 15 ((Fun # ∧ (𝑓 ∪ {𝐵}) ∈ dom #) → ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} → (#‘(𝑓 ∪ {𝐵})) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})))
1643, 162, 163mp2an 707 . . . . . . . . . . . . . 14 ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} → (#‘(𝑓 ∪ {𝐵})) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
165157, 164syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘(𝑓 ∪ {𝐵})) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
16645, 165eqeltrrd 2699 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((#‘𝑓) + 1) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
167 ne0i 3902 . . . . . . . . . . . 12 (((#‘𝑓) + 1) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) → (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅)
168166, 167syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅)
16923simpli 474 . . . . . . . . . . . 12 (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin
170 fimaxre2 10921 . . . . . . . . . . . 12 (((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ ∧ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧)
17127, 169, 170sylancl 693 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧)
172 suprub 10936 . . . . . . . . . . 11 ((((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ ∧ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧) ∧ ((#‘𝑓) + 1) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})) → ((#‘𝑓) + 1) ≤ sup((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
17327, 168, 171, 166, 172syl31anc 1326 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((#‘𝑓) + 1) ≤ sup((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
1745, 6, 7erdszelem3 30918 . . . . . . . . . . . 12 (𝐵 ∈ (1...𝑁) → (𝐾𝐵) = sup((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
17532, 174syl 17 . . . . . . . . . . 11 (𝜑 → (𝐾𝐵) = sup((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
176175ad2antrr 761 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) = sup((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
177173, 176breqtrrd 4646 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((#‘𝑓) + 1) ≤ (𝐾𝐵))
1785, 6, 7, 8erdszelem6 30921 . . . . . . . . . . . . 13 (𝜑𝐾:(1...𝑁)⟶ℕ)
179178, 32ffvelrnd 6321 . . . . . . . . . . . 12 (𝜑 → (𝐾𝐵) ∈ ℕ)
180179ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) ∈ ℕ)
181180nnnn0d 11303 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) ∈ ℕ0)
182 nn0ltp1le 11387 . . . . . . . . . 10 (((#‘𝑓) ∈ ℕ0 ∧ (𝐾𝐵) ∈ ℕ0) → ((#‘𝑓) < (𝐾𝐵) ↔ ((#‘𝑓) + 1) ≤ (𝐾𝐵)))
18320, 181, 182syl2anc 692 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((#‘𝑓) < (𝐾𝐵) ↔ ((#‘𝑓) + 1) ≤ (𝐾𝐵)))
184177, 183mpbird 247 . . . . . . . 8 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘𝑓) < (𝐾𝐵))
18521, 184ltned 10125 . . . . . . 7 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘𝑓) ≠ (𝐾𝐵))
186185ex 450 . . . . . 6 ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) → ((𝐹𝐴)𝑂(𝐹𝐵) → (#‘𝑓) ≠ (𝐾𝐵)))
187 neeq1 2852 . . . . . . 7 ((#‘𝑓) = (𝐾𝐴) → ((#‘𝑓) ≠ (𝐾𝐵) ↔ (𝐾𝐴) ≠ (𝐾𝐵)))
188187imbi2d 330 . . . . . 6 ((#‘𝑓) = (𝐾𝐴) → (((𝐹𝐴)𝑂(𝐹𝐵) → (#‘𝑓) ≠ (𝐾𝐵)) ↔ ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
189186, 188syl5ibcom 235 . . . . 5 ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) → ((#‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
19014, 189sylan2b 492 . . . 4 ((𝜑𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}) → ((#‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
191190rexlimdva 3025 . . 3 (𝜑 → (∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (#‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
19212, 191mpd 15 . 2 (𝜑 → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵)))
193192necon2bd 2806 1 (𝜑 → ((𝐾𝐴) = (𝐾𝐵) → ¬ (𝐹𝐴)𝑂(𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  cun 3557  wss 3559  c0 3896  𝒫 cpw 4135  {csn 4153   class class class wbr 4618  cmpt 4678   Or wor 4999  dom cdm 5079  cres 5081  cima 5082  Fun wfun 5846  wf 5848  1-1wf1 5849  cfv 5852   Isom wiso 5853  (class class class)co 6610  Fincfn 7907  supcsup 8298  cr 9887  1c1 9889   + caddc 9891  +∞cpnf 10023   < clt 10026  cle 10027  cn 10972  0cn0 11244  cz 11329  cuz 11639  ...cfz 12276  #chash 13065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-sup 8300  df-card 8717  df-cda 8942  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-nn 10973  df-n0 11245  df-xnn0 11316  df-z 11330  df-uz 11640  df-fz 12277  df-hash 13066
This theorem is referenced by:  erdszelem9  30924
  Copyright terms: Public domain W3C validator