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 31458
Description: Lemma for erdsze 31462. (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 13290 . . . . 5 ♯:V⟶(ℕ0 ∪ {+∞})
2 ffun 6197 . . . . 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 31455 . . . . 5 ((𝜑𝐴 ∈ (1...𝑁)) → (𝐾𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}))
104, 9mpdan 705 . . . 4 (𝜑 → (𝐾𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}))
11 fvelima 6398 . . . 4 ((Fun ♯ ∧ (𝐾𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)})) → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (♯‘𝑓) = (𝐾𝐴))
123, 10, 11sylancr 698 . . 3 (𝜑 → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (♯‘𝑓) = (𝐾𝐴))
13 eqid 2748 . . . . . 6 {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}
1413erdszelem1 31451 . . . . 5 (𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} ↔ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓))
15 fzfid 12937 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ∈ Fin)
16 simplr1 1237 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝐴))
17 ssfi 8333 . . . . . . . . . . 11 (((1...𝐴) ∈ Fin ∧ 𝑓 ⊆ (1...𝐴)) → 𝑓 ∈ Fin)
1815, 16, 17syl2anc 696 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ∈ Fin)
19 hashcl 13310 . . . . . . . . . 10 (𝑓 ∈ Fin → (♯‘𝑓) ∈ ℕ0)
2018, 19syl 17 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) ∈ ℕ0)
2120nn0red 11515 . . . . . . . 8 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) ∈ ℝ)
22 eqid 2748 . . . . . . . . . . . . . . 15 {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} = {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}
2322erdszelem2 31452 . . . . . . . . . . . . . 14 ((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℕ)
2423simpri 481 . . . . . . . . . . . . 13 (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℕ
25 nnssre 11187 . . . . . . . . . . . . 13 ℕ ⊆ ℝ
2624, 25sstri 3741 . . . . . . . . . . . 12 (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ
2726a1i 11 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ)
28 erdszelem.l . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 < 𝐵)
29 elfznn 12534 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ)
304, 29syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℕ)
3130nnred 11198 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐴 ∈ ℝ)
32 erdszelem.b . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐵 ∈ (1...𝑁))
33 elfznn 12534 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℕ)
3432, 33syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℕ)
3534nnred 11198 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ ℝ)
3631, 35ltnled 10347 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
3728, 36mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑 → ¬ 𝐵𝐴)
38 elfzle2 12509 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (1...𝐴) → 𝐵𝐴)
3937, 38nsyl 135 . . . . . . . . . . . . . . . 16 (𝜑 → ¬ 𝐵 ∈ (1...𝐴))
4039ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ¬ 𝐵 ∈ (1...𝐴))
4116, 40ssneldd 3735 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ¬ 𝐵𝑓)
4232ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (1...𝑁))
43 hashunsng 13344 . . . . . . . . . . . . . . 15 (𝐵 ∈ (1...𝑁) → ((𝑓 ∈ Fin ∧ ¬ 𝐵𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
4442, 43syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝑓 ∈ Fin ∧ ¬ 𝐵𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
4518, 41, 44mp2and 717 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1))
46 elfzelz 12506 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℤ)
474, 46syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴 ∈ ℤ)
48 elfzelz 12506 . . . . . . . . . . . . . . . . . . . . 21 (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℤ)
4932, 48syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐵 ∈ ℤ)
5031, 35, 28ltled 10348 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝐴𝐵)
51 eluz2 11856 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ (ℤ𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴𝐵))
5247, 49, 50, 51syl3anbrc 1407 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ∈ (ℤ𝐴))
53 fzss2 12545 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ (ℤ𝐴) → (1...𝐴) ⊆ (1...𝐵))
5452, 53syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1...𝐴) ⊆ (1...𝐵))
5554ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ⊆ (1...𝐵))
5616, 55sstrd 3742 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝐵))
57 elfz1end 12535 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵))
5834, 57sylib 208 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ (1...𝐵))
5958ad2antrr 764 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (1...𝐵))
6059snssd 4473 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → {𝐵} ⊆ (1...𝐵))
6156, 60unssd 3920 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝐵))
62 simplr2 1239 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)))
63 f1f 6250 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ)
646, 63syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐹:(1...𝑁)⟶ℝ)
6564ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐹:(1...𝑁)⟶ℝ)
66 elfzuz3 12503 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ𝐴))
67 fzss2 12545 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ (ℤ𝐴) → (1...𝐴) ⊆ (1...𝑁))
684, 66, 673syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → (1...𝐴) ⊆ (1...𝑁))
6968ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (1...𝐴) ⊆ (1...𝑁))
7016, 69sstrd 3742 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝑓 ⊆ (1...𝑁))
71 fzssuz 12546 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1...𝑁) ⊆ (ℤ‘1)
72 uzssz 11870 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (ℤ‘1) ⊆ ℤ
73 zssre 11547 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ℤ ⊆ ℝ
7472, 73sstri 3741 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ℤ‘1) ⊆ ℝ
7571, 74sstri 3741 . . . . . . . . . . . . . . . . . . . . . . . 24 (1...𝑁) ⊆ ℝ
76 ltso 10281 . . . . . . . . . . . . . . . . . . . . . . . 24 < Or ℝ
77 soss 5193 . . . . . . . . . . . . . . . . . . . . . . . 24 ((1...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (1...𝑁)))
7875, 76, 77mp2 9 . . . . . . . . . . . . . . . . . . . . . . 23 < Or (1...𝑁)
79 soisores 6728 . . . . . . . . . . . . . . . . . . . . . . 23 ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁))) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
8078, 8, 79mpanl12 720 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁)) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
8165, 70, 80syl2anc 696 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ↔ ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
8262, 81mpbid 222 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧𝑓𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
8382r19.21bi 3058 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
8416sselda 3732 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ (1...𝐴))
85 elfzle2 12509 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑧 ∈ (1...𝐴) → 𝑧𝐴)
8684, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧𝐴)
8770sselda 3732 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ (1...𝑁))
8875, 87sseldi 3730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧 ∈ ℝ)
894ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ (1...𝑁))
9089, 29syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ ℕ)
9190nnred 11198 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴 ∈ ℝ)
9288, 91lenltd 10346 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑧𝐴 ↔ ¬ 𝐴 < 𝑧))
9386, 92mpbid 222 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ¬ 𝐴 < 𝑧)
9462adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)))
95 simplr3 1241 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐴𝑓)
9695adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐴𝑓)
97 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝑧𝑓)
98 isorel 6727 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (𝐴 < 𝑧 ↔ ((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧)))
99 fvres 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝐴𝑓 → ((𝐹𝑓)‘𝐴) = (𝐹𝐴))
100 fvres 6356 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑧𝑓 → ((𝐹𝑓)‘𝑧) = (𝐹𝑧))
10199, 100breqan12d 4808 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐴𝑓𝑧𝑓) → (((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧) ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
102101adantl 473 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (((𝐹𝑓)‘𝐴)𝑂((𝐹𝑓)‘𝑧) ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
10398, 102bitrd 268 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ (𝐴𝑓𝑧𝑓)) → (𝐴 < 𝑧 ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
10494, 96, 97, 103syl12anc 1461 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐴 < 𝑧 ↔ (𝐹𝐴)𝑂(𝐹𝑧)))
10593, 104mtbid 313 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ¬ (𝐹𝐴)𝑂(𝐹𝑧))
106 simplr 809 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐴)𝑂(𝐹𝐵))
10765adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐹:(1...𝑁)⟶ℝ)
108107, 87ffvelrnd 6511 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑧) ∈ ℝ)
109107, 89ffvelrnd 6511 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐴) ∈ ℝ)
11042adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → 𝐵 ∈ (1...𝑁))
111107, 110ffvelrnd 6511 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝐵) ∈ ℝ)
112 sotr2 5204 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 Or ℝ ∧ ((𝐹𝑧) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ)) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
1138, 112mpan 708 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑧) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐹𝐵) ∈ ℝ) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
114108, 109, 111, 113syl3anc 1463 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ((¬ (𝐹𝐴)𝑂(𝐹𝑧) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹𝑧)𝑂(𝐹𝐵)))
115105, 106, 114mp2and 717 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝐹𝑧)𝑂(𝐹𝐵))
116115a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝐵)))
117 elsni 4326 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ {𝐵} → 𝑤 = 𝐵)
118117fveq2d 6344 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ {𝐵} → (𝐹𝑤) = (𝐹𝐵))
119118breq2d 4804 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ {𝐵} → ((𝐹𝑧)𝑂(𝐹𝑤) ↔ (𝐹𝑧)𝑂(𝐹𝐵)))
120119imbi2d 329 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝐵))))
121116, 120syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → (𝑤 ∈ {𝐵} → (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
122121ralrimiv 3091 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
123 ralunb 3925 . . . . . . . . . . . . . . . . . . 19 (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (∀𝑤𝑓 (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ∧ ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
12483, 122, 123sylanbrc 701 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑧𝑓) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
125124ralrimiva 3092 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧𝑓𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
12661sselda 3732 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → 𝑤 ∈ (1...𝐵))
127 elfzle2 12509 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ (1...𝐵) → 𝑤𝐵)
128127adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤𝐵)
129 elfzelz 12506 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℤ)
130129zred 11645 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℝ)
131130adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ∈ ℝ)
13235ad3antrrr 768 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝐵 ∈ ℝ)
133131, 132lenltd 10346 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → (𝑤𝐵 ↔ ¬ 𝐵 < 𝑤))
134128, 133mpbid 222 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → ¬ 𝐵 < 𝑤)
135126, 134syldan 488 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → ¬ 𝐵 < 𝑤)
136135pm2.21d 118 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → (𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
137136ralrimiva 3092 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
138 elsni 4326 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
139138breq1d 4802 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 ∈ {𝐵} → (𝑧 < 𝑤𝐵 < 𝑤))
140139imbi1d 330 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
141140ralbidv 3112 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ {𝐵} → (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
142137, 141syl5ibrcom 237 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑧 ∈ {𝐵} → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
143142ralrimiv 3091 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
144 ralunb 3925 . . . . . . . . . . . . . . . . 17 (∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ↔ (∀𝑧𝑓𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)) ∧ ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
145125, 143, 144sylanbrc 701 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤)))
14642snssd 4473 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → {𝐵} ⊆ (1...𝑁))
14770, 146unssd 3920 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))
148 soisores 6728 . . . . . . . . . . . . . . . . . 18 ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
14978, 8, 148mpanl12 720 . . . . . . . . . . . . . . . . 17 ((𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
15065, 147, 149syl2anc 696 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹𝑧)𝑂(𝐹𝑤))))
151145, 150mpbird 247 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))))
152 ssun2 3908 . . . . . . . . . . . . . . . 16 {𝐵} ⊆ (𝑓 ∪ {𝐵})
153 snssg 4447 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ (1...𝐵) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
15459, 153syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
155152, 154mpbiri 248 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → 𝐵 ∈ (𝑓 ∪ {𝐵}))
15622erdszelem1 31451 . . . . . . . . . . . . . . 15 ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} ↔ ((𝑓 ∪ {𝐵}) ⊆ (1...𝐵) ∧ (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ∧ 𝐵 ∈ (𝑓 ∪ {𝐵})))
15761, 151, 155, 156syl3anbrc 1407 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})
158 vex 3331 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
159 snex 5045 . . . . . . . . . . . . . . . . 17 {𝐵} ∈ V
160158, 159unex 7109 . . . . . . . . . . . . . . . 16 (𝑓 ∪ {𝐵}) ∈ V
1611fdmi 6201 . . . . . . . . . . . . . . . 16 dom ♯ = V
162160, 161eleqtrri 2826 . . . . . . . . . . . . . . 15 (𝑓 ∪ {𝐵}) ∈ dom ♯
163 funfvima 6643 . . . . . . . . . . . . . . 15 ((Fun ♯ ∧ (𝑓 ∪ {𝐵}) ∈ dom ♯) → ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})))
1643, 162, 163mp2an 710 . . . . . . . . . . . . . 14 ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
165157, 164syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
16645, 165eqeltrrd 2828 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}))
167 ne0i 4052 . . . . . . . . . . . 12 (((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅)
168166, 167syl 17 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅)
16923simpli 476 . . . . . . . . . . . 12 (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin
170 fimaxre2 11132 . . . . . . . . . . . 12 (((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧)
17127, 169, 170sylancl 697 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧)
172 suprub 11147 . . . . . . . . . . 11 ((((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})𝑤𝑧) ∧ ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)})) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
17327, 168, 171, 166, 172syl31anc 1466 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
1745, 6, 7erdszelem3 31453 . . . . . . . . . . . 12 (𝐵 ∈ (1...𝑁) → (𝐾𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
17532, 174syl 17 . . . . . . . . . . 11 (𝜑 → (𝐾𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
176175ad2antrr 764 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐵𝑦)}), ℝ, < ))
177173, 176breqtrrd 4820 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) + 1) ≤ (𝐾𝐵))
1785, 6, 7, 8erdszelem6 31456 . . . . . . . . . . . . 13 (𝜑𝐾:(1...𝑁)⟶ℕ)
179178, 32ffvelrnd 6511 . . . . . . . . . . . 12 (𝜑 → (𝐾𝐵) ∈ ℕ)
180179ad2antrr 764 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) ∈ ℕ)
181180nnnn0d 11514 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (𝐾𝐵) ∈ ℕ0)
182 nn0ltp1le 11598 . . . . . . . . . 10 (((♯‘𝑓) ∈ ℕ0 ∧ (𝐾𝐵) ∈ ℕ0) → ((♯‘𝑓) < (𝐾𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾𝐵)))
18320, 181, 182syl2anc 696 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → ((♯‘𝑓) < (𝐾𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾𝐵)))
184177, 183mpbird 247 . . . . . . . 8 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) < (𝐾𝐵))
18521, 184ltned 10336 . . . . . . 7 (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) ∧ (𝐹𝐴)𝑂(𝐹𝐵)) → (♯‘𝑓) ≠ (𝐾𝐵))
186185ex 449 . . . . . 6 ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) → ((𝐹𝐴)𝑂(𝐹𝐵) → (♯‘𝑓) ≠ (𝐾𝐵)))
187 neeq1 2982 . . . . . . 7 ((♯‘𝑓) = (𝐾𝐴) → ((♯‘𝑓) ≠ (𝐾𝐵) ↔ (𝐾𝐴) ≠ (𝐾𝐵)))
188187imbi2d 329 . . . . . 6 ((♯‘𝑓) = (𝐾𝐴) → (((𝐹𝐴)𝑂(𝐹𝐵) → (♯‘𝑓) ≠ (𝐾𝐵)) ↔ ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
189186, 188syl5ibcom 235 . . . . 5 ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹𝑓) Isom < , 𝑂 (𝑓, (𝐹𝑓)) ∧ 𝐴𝑓)) → ((♯‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
19014, 189sylan2b 493 . . . 4 ((𝜑𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)}) → ((♯‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
191190rexlimdva 3157 . . 3 (𝜑 → (∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹𝑦) Isom < , 𝑂 (𝑦, (𝐹𝑦)) ∧ 𝐴𝑦)} (♯‘𝑓) = (𝐾𝐴) → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵))))
19212, 191mpd 15 . 2 (𝜑 → ((𝐹𝐴)𝑂(𝐹𝐵) → (𝐾𝐴) ≠ (𝐾𝐵)))
193192necon2bd 2936 1 (𝜑 → ((𝐾𝐴) = (𝐾𝐵) → ¬ (𝐹𝐴)𝑂(𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1620  wcel 2127  wne 2920  wral 3038  wrex 3039  {crab 3042  Vcvv 3328  cun 3701  wss 3703  c0 4046  𝒫 cpw 4290  {csn 4309   class class class wbr 4792  cmpt 4869   Or wor 5174  dom cdm 5254  cres 5256  cima 5257  Fun wfun 6031  wf 6033  1-1wf1 6034  cfv 6037   Isom wiso 6038  (class class class)co 6801  Fincfn 8109  supcsup 8499  cr 10098  1c1 10100   + caddc 10102  +∞cpnf 10234   < clt 10237  cle 10238  cn 11183  0cn0 11455  cz 11540  cuz 11850  ...cfz 12490  chash 13282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-rep 4911  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-cnex 10155  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-mulcom 10163  ax-addass 10164  ax-mulass 10165  ax-distr 10166  ax-i2m1 10167  ax-1ne0 10168  ax-1rid 10169  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172  ax-pre-lttri 10173  ax-pre-lttrn 10174  ax-pre-ltadd 10175  ax-pre-mulgt0 10176  ax-pre-sup 10177
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-reu 3045  df-rmo 3046  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-int 4616  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-isom 6046  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-om 7219  df-1st 7321  df-2nd 7322  df-wrecs 7564  df-recs 7625  df-rdg 7663  df-1o 7717  df-2o 7718  df-oadd 7721  df-er 7899  df-map 8013  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-sup 8501  df-card 8926  df-cda 9153  df-pnf 10239  df-mnf 10240  df-xr 10241  df-ltxr 10242  df-le 10243  df-sub 10431  df-neg 10432  df-nn 11184  df-n0 11456  df-xnn0 11527  df-z 11541  df-uz 11851  df-fz 12491  df-hash 13283
This theorem is referenced by:  erdszelem9  31459
  Copyright terms: Public domain W3C validator