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

Theorem erdszelem8 30434
 Description: Lemma for erdsze 30438. (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 12987 . . . . 5 #:V⟶(ℕ0 ∪ {+∞})
2 ffun 5961 . . . . 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 30431 . . . . 5 ((𝜑𝐴 ∈ (1...𝑁)) → (𝐾𝐴) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}))
104, 9mpdan 699 . . . 4 (𝜑 → (𝐾𝐴) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}))
11 fvelima 6158 . . . 4 ((Fun # ∧ (𝐾𝐴) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)})) → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (#‘𝑓) = (𝐾𝐴))
123, 10, 11sylancr 694 . . 3 (𝜑 → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (#‘𝑓) = (𝐾𝐴))
13 eqid 2610 . . . . . 6 {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}
1413erdszelem1 30427 . . . . 5 (𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} ↔ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓))
15 fzfid 12634 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ∈ Fin)
16 simplr1 1096 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝐴))
17 ssfi 8065 . . . . . . . . . . 11 (((1...𝐴) ∈ Fin ∧ 𝑓 ⊆ (1...𝐴)) → 𝑓 ∈ Fin)
1815, 16, 17syl2anc 691 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ∈ Fin)
19 hashcl 13009 . . . . . . . . . 10 (𝑓 ∈ Fin → (#‘𝑓) ∈ ℕ0)
2018, 19syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘𝑓) ∈ ℕ0)
2120nn0red 11229 . . . . . . . 8 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘𝑓) ∈ ℝ)
22 eqid 2610 . . . . . . . . . . . . . . 15 {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} = {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}
2322erdszelem2 30428 . . . . . . . . . . . . . 14 ((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin ∧ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℕ)
2423simpri 477 . . . . . . . . . . . . 13 (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℕ
25 nnssre 10901 . . . . . . . . . . . . 13 ℕ ⊆ ℝ
2624, 25sstri 3577 . . . . . . . . . . . 12 (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ
2726a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ)
28 erdszelem.l . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 < 𝐵)
29 elfznn 12241 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ)
304, 29syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℕ)
3130nnred 10912 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
32 erdszelem.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ (1...𝑁))
33 elfznn 12241 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℕ)
3432, 33syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℕ)
3534nnred 10912 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ)
3631, 35ltnled 10063 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
3728, 36mpbid 221 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ 𝐵𝐴)
38 elfzle2 12216 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (1...𝐴) → 𝐵𝐴)
3937, 38nsyl 134 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ 𝐵 ∈ (1...𝐴))
4039ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ¬ 𝐵 ∈ (1...𝐴))
4116, 40ssneldd 3571 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ¬ 𝐵𝑓)
4232ad2antrr 758 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (1...𝑁))
43 hashunsng 13042 . . . . . . . . . . . . . . 15 (𝐵 ∈ (1...𝑁) → ((𝑓 ∈ Fin ∧ ¬ 𝐵𝑓) → (#‘(𝑓 ∪ {𝐵})) = ((#‘𝑓) + 1)))
4442, 43syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝑓 ∈ Fin ∧ ¬ 𝐵𝑓) → (#‘(𝑓 ∪ {𝐵})) = ((#‘𝑓) + 1)))
4518, 41, 44mp2and 711 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘(𝑓 ∪ {𝐵})) = ((#‘𝑓) + 1))
46 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℤ)
474, 46syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℤ)
48 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℤ)
4932, 48syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℤ)
5031, 35, 28ltled 10064 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴𝐵)
51 eluz2 11569 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ (ℤ𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴𝐵))
5247, 49, 50, 51syl3anbrc 1239 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ (ℤ𝐴))
53 fzss2 12252 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (ℤ𝐴) → (1...𝐴) ⊆ (1...𝐵))
5452, 53syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...𝐴) ⊆ (1...𝐵))
5554ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ⊆ (1...𝐵))
5616, 55sstrd 3578 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝐵))
57 elfz1end 12242 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵))
5834, 57sylib 207 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ (1...𝐵))
5958ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (1...𝐵))
6059snssd 4281 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → {𝐵} ⊆ (1...𝐵))
6156, 60unssd 3751 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝐵))
62 simplr2 1097 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)))
63 f1f 6014 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ)
646, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹:(1...𝑁)⟶ℝ)
6564ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐹:(1...𝑁)⟶ℝ)
66 elfzuz3 12210 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ𝐴))
67 fzss2 12252 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ𝐴) → (1...𝐴) ⊆ (1...𝑁))
684, 66, 673syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...𝐴) ⊆ (1...𝑁))
6968ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ⊆ (1...𝑁))
7016, 69sstrd 3578 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝑁))
71 fzssuz 12253 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...𝑁) ⊆ (ℤ‘1)
72 uzssz 11583 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ℤ‘1) ⊆ ℤ
73 zssre 11261 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℤ ⊆ ℝ
7472, 73sstri 3577 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℤ‘1) ⊆ ℝ
7571, 74sstri 3577 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑁) ⊆ ℝ
76 ltso 9997 . . . . . . . . . . . . . . . . . . . . . . . 24 < Or ℝ
77 soss 4977 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (1...𝑁)))
7875, 76, 77mp2 9 . . . . . . . . . . . . . . . . . . . . . . 23 < Or (1...𝑁)
79 soisores 6477 . . . . . . . . . . . . . . . . . . . . . . 23 ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁))) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
8078, 8, 79mpanl12 714 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁)) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
8165, 70, 80syl2anc 691 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
8262, 81mpbid 221 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
8382r19.21bi 2916 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
8416sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ (1...𝐴))
85 elfzle2 12216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ (1...𝐴) → 𝑧𝐴)
8684, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧𝐴)
8770sselda 3568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ (1...𝑁))
8875, 87sseldi 3566 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ ℝ)
894ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ (1...𝑁))
9089, 29syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ ℕ)
9190nnred 10912 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ ℝ)
9288, 91lenltd 10062 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑧𝐴 ↔ ¬ 𝐴 < 𝑧))
9386, 92mpbid 221 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ¬ 𝐴 < 𝑧)
9462adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)))
95 simplr3 1098 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐴𝑓)
9695adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴𝑓)
97 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧𝑓)
98 isorel 6476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (𝐴 < 𝑧 ↔ ((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧)))
99 fvres 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴𝑓 → ((𝐹𝑓)‘𝐴) = (𝐹𝐴))
100 fvres 6117 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧𝑓 → ((𝐹𝑓)‘𝑧) = (𝐹𝑧))
10199, 100breqan12d 4599 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴𝑓𝑧𝑓) → (((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧) ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
102101adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧) ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
10398, 102bitrd 267 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (𝐴 < 𝑧 ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
10494, 96, 97, 103syl12anc 1316 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐴 < 𝑧 ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
10593, 104mtbid 313 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ¬ (𝐹𝐴)𝑂(𝐹𝑧))
106 simplr 788 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐴)𝑂(𝐹𝐵))
10765adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐹:(1...𝑁)⟶ℝ)
108107, 87ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑧) ∈ ℝ)
109107, 89ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐴) ∈ ℝ)
11042adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐵 ∈ (1...𝑁))
111107, 110ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐵) ∈ ℝ)
112 sotr2 4988 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 Or ℝ ∧ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ)) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
1138, 112mpan 702 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑧) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
114108, 109, 111, 113syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
115105, 106, 114mp2and 711 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑧)𝑂(𝐹𝐵))
116115a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝐵)))
117 elsni 4142 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ {𝐵} → 𝑤 = 𝐵)
118117fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ {𝐵} → (𝐹𝑤) = (𝐹𝐵))
119118breq2d 4595 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ {𝐵} → ((𝐹𝑧)𝑂(𝐹𝑤) ↔ (𝐹𝑧)𝑂(𝐹𝐵)))
120119imbi2d 329 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝐵))))
121116, 120syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑤 ∈ {𝐵} → (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
122121ralrimiv 2948 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
123 ralunb 3756 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (∀𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ∧ ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
12483, 122, 123sylanbrc 695 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
125124ralrimiva 2949 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧𝑓𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
12661sselda 3568 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → 𝑤 ∈ (1...𝐵))
127 elfzle2 12216 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ (1...𝐵) → 𝑤𝐵)
128127adantl 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤𝐵)
129 elfzelz 12213 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℤ)
130129zred 11358 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℝ)
131130adantl 481 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ∈ ℝ)
13235ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝐵 ∈ ℝ)
133131, 132lenltd 10062 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → (𝑤𝐵 ↔ ¬ 𝐵 < 𝑤))
134128, 133mpbid 221 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → ¬ 𝐵 < 𝑤)
135126, 134syldan 486 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → ¬ 𝐵 < 𝑤)
136135pm2.21d 117 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → (𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
137136ralrimiva 2949 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
138 elsni 4142 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
139138breq1d 4593 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ {𝐵} → (𝑧 < 𝑤𝐵 < 𝑤))
140139imbi1d 330 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
141140ralbidv 2969 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ {𝐵} → (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
142137, 141syl5ibrcom 236 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑧 ∈ {𝐵} → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
143142ralrimiv 2948 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
144 ralunb 3756 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (∀𝑧𝑓𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ∧ ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
145125, 143, 144sylanbrc 695 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
14642snssd 4281 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → {𝐵} ⊆ (1...𝑁))
14770, 146unssd 3751 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))
148 soisores 6477 . . . . . . . . . . . . . . . . . 18 ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
14978, 8, 148mpanl12 714 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
15065, 147, 149syl2anc 691 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
151145, 150mpbird 246 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))))
152 ssun2 3739 . . . . . . . . . . . . . . . 16 {𝐵} ⊆ (𝑓 ∪ {𝐵})
153 snssg 4268 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (1...𝐵) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
15459, 153syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
155152, 154mpbiri 247 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (𝑓 ∪ {𝐵}))
15622erdszelem1 30427 . . . . . . . . . . . . . . 15 ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} ↔ ((𝑓 ∪ {𝐵}) ⊆ (1...𝐵) ∧ (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ∧ 𝐵 ∈ (𝑓 ∪ {𝐵})))
15761, 151, 155, 156syl3anbrc 1239 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})
158 vex 3176 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
159 snex 4835 . . . . . . . . . . . . . . . . 17 {𝐵} ∈ V
160158, 159unex 6854 . . . . . . . . . . . . . . . 16 (𝑓 ∪ {𝐵}) ∈ V
1611fdmi 5965 . . . . . . . . . . . . . . . 16 dom # = V
162160, 161eleqtrri 2687 . . . . . . . . . . . . . . 15 (𝑓 ∪ {𝐵}) ∈ dom #
163 funfvima 6396 . . . . . . . . . . . . . . 15 ((Fun # ∧ (𝑓 ∪ {𝐵}) ∈ dom #) → ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} → (#‘(𝑓 ∪ {𝐵})) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})))
1643, 162, 163mp2an 704 . . . . . . . . . . . . . 14 ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} → (#‘(𝑓 ∪ {𝐵})) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
165157, 164syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘(𝑓 ∪ {𝐵})) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
16645, 165eqeltrrd 2689 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((#‘𝑓) + 1) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
167 ne0i 3880 . . . . . . . . . . . 12 (((#‘𝑓) + 1) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) → (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅)
168166, 167syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅)
16923simpli 473 . . . . . . . . . . . 12 (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin
170 fimaxre2 10848 . . . . . . . . . . . 12 (((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ ∧ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧)
17127, 169, 170sylancl 693 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧)
172 suprub 10863 . . . . . . . . . . 11 ((((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ ∧ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧) ∧ ((#‘𝑓) + 1) ∈ (# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})) → ((#‘𝑓) + 1) ≤ sup((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
17327, 168, 171, 166, 172syl31anc 1321 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((#‘𝑓) + 1) ≤ sup((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
1745, 6, 7erdszelem3 30429 . . . . . . . . . . . 12 (𝐵 ∈ (1...𝑁) → (𝐾𝐵) = sup((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
17532, 174syl 17 . . . . . . . . . . 11 (𝜑 → (𝐾𝐵) = sup((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
176175ad2antrr 758 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) = sup((# “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
177173, 176breqtrrd 4611 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((#‘𝑓) + 1) ≤ (𝐾𝐵))
1785, 6, 7, 8erdszelem6 30432 . . . . . . . . . . . . 13 (𝜑𝐾:(1...𝑁)⟶ℕ)
179178, 32ffvelrnd 6268 . . . . . . . . . . . 12 (𝜑 → (𝐾𝐵) ∈ ℕ)
180179ad2antrr 758 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) ∈ ℕ)
181180nnnn0d 11228 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) ∈ ℕ0)
182 nn0ltp1le 11312 . . . . . . . . . 10 (((#‘𝑓) ∈ ℕ0 ∧ (𝐾𝐵) ∈ ℕ0) → ((#‘𝑓) < (𝐾𝐵) ↔ ((#‘𝑓) + 1) ≤ (𝐾𝐵)))
18320, 181, 182syl2anc 691 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((#‘𝑓) < (𝐾𝐵) ↔ ((#‘𝑓) + 1) ≤ (𝐾𝐵)))
184177, 183mpbird 246 . . . . . . . 8 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘𝑓) < (𝐾𝐵))
18521, 184ltned 10052 . . . . . . 7 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (#‘𝑓) ≠ (𝐾𝐵))
186185ex 449 . . . . . 6 ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) → ((𝐹𝐴)𝑂(𝐹𝐵) → (#‘𝑓) ≠ (𝐾𝐵)))
187 neeq1 2844 . . . . . . 7 ((#‘𝑓) = (𝐾𝐴) → ((#‘𝑓) ≠ (𝐾𝐵) ↔ (𝐾𝐴) ≠ (𝐾𝐵)))
188187imbi2d 329 . . . . . 6 ((#‘𝑓) = (𝐾𝐴) → (((𝐹𝐴)𝑂(𝐹𝐵) → (#‘𝑓) ≠ (𝐾𝐵)) ↔ ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
189186, 188syl5ibcom 234 . . . . 5 ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) → ((#‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
19014, 189sylan2b 491 . . . 4 ((𝜑𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}) → ((#‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
191190rexlimdva 3013 . . 3 (𝜑 → (∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (#‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
19212, 191mpd 15 . 2 (𝜑 → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵)))
193192necon2bd 2798 1 (𝜑 → ((𝐾𝐴) = (𝐾𝐵) → ¬ (𝐹𝐴)𝑂(𝐹𝐵)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∪ cun 3538   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   Or wor 4958  dom cdm 5038   ↾ cres 5040   “ cima 5041  Fun wfun 5798  ⟶wf 5800  –1-1→wf1 5801  ‘cfv 5804   Isom wiso 5805  (class class class)co 6549  Fincfn 7841  supcsup 8229  ℝcr 9814  1c1 9816   + caddc 9818  +∞cpnf 9950   < clt 9953   ≤ cle 9954  ℕcn 10897  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ...cfz 12197  #chash 12979 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-sup 8231  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-xnn0 11241  df-z 11255  df-uz 11564  df-fz 12198  df-hash 12980 This theorem is referenced by:  erdszelem9  30435
 Copyright terms: Public domain W3C validator