erdszelem8 - Mathbox for Mario Carneiro

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

Theorem erdszelem8 34020

Description: Lemma for erdsze 34024. (Contributed by Mario Carneiro, 22-Jan-2015.)

**Hypotheses**
Ref	Expression
erdsze.n	⊢ (𝜑 → 𝑁 ∈ ℕ)
erdsze.f	⊢ (𝜑 → 𝐹:(1...𝑁)–1-1→ℝ)
erdszelem.k	⊢ 𝐾 = (𝑥 ∈ (1...𝑁) ↦ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝑥) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝑥 ∈ 𝑦)}), ℝ, < ))
erdszelem.o	⊢ 𝑂 Or ℝ
erdszelem.a	⊢ (𝜑 → 𝐴 ∈ (1...𝑁))
erdszelem.b	⊢ (𝜑 → 𝐵 ∈ (1...𝑁))
erdszelem.l	⊢ (𝜑 → 𝐴 < 𝐵)

**Assertion**
Ref	Expression
erdszelem8	⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵)))

Distinct variable groups: 𝑥,𝑦,𝐵 𝑥,𝐹,𝑦 𝑥,𝐴,𝑦 𝑥,𝑂,𝑦 𝑥,𝑁,𝑦 𝜑,𝑥,𝑦 Allowed substitution hints: 𝐾(𝑥,𝑦)

Proof of Theorem erdszelem8 Dummy variables 𝑤 𝑓 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hashf 14280	. . . . 5 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
2		ffun 6707	. . . . 5 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → Fun ♯)
3	1, 2	ax-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 ℝ
9	5, 6, 7, 8	erdszelem5 34017	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
10	4, 9	mpdan 685	. . . 4 ⊢ (𝜑 → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
11		fvelima 6944	. . . 4 ⊢ ((Fun ♯ ∧ (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})) → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴))
12	3, 10, 11	sylancr 587	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴))
13		eqid 2731	. . . . . 6 ⊢ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}
14	13	erdszelem1 34013	. . . . 5 ⊢ (𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} ↔ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓))
15		fzfid 13920	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ∈ Fin)
16		simplr1 1215	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝐴))
17		ssfi 9156	. . . . . . . . . . 11 ⊢ (((1...𝐴) ∈ Fin ∧ 𝑓 ⊆ (1...𝐴)) → 𝑓 ∈ Fin)
18	15, 16, 17	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ∈ Fin)
19		hashcl 14298	. . . . . . . . . 10 ⊢ (𝑓 ∈ Fin → (♯‘𝑓) ∈ ℕ₀)
20	18, 19	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ∈ ℕ₀)
21	20	nn0red 12515	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ∈ ℝ)
22		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}
23	22	erdszelem2 34014	. . . . . . . . . . . . . 14 ⊢ ((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℕ)
24	23	simpri 486	. . . . . . . . . . . . 13 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℕ
25		nnssre 12198	. . . . . . . . . . . . 13 ⊢ ℕ ⊆ ℝ
26	24, 25	sstri 3987	. . . . . . . . . . . 12 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ
27	26	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ)
28	4	elfzelzd 13484	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℤ)
29		erdszelem.b	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (1...𝑁))
30	29	elfzelzd 13484	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ ℤ)
31		elfznn 13512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ)
32	4, 31	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℕ)
33	32	nnred 12209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℝ)
34		elfznn 13512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℕ)
35	29, 34	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℕ)
36	35	nnred 12209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℝ)
37		erdszelem.l	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 < 𝐵)
38	33, 36, 37	ltled 11344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
39		eluz2 12810	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵))
40	28, 30, 38, 39	syl3anbrc 1343	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘𝐴))
41		fzss2 13523	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (1...𝐴) ⊆ (1...𝐵))
42	40, 41	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝐴) ⊆ (1...𝐵))
43	42	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ⊆ (1...𝐵))
44	16, 43	sstrd 3988	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝐵))
45		elfz1end 13513	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵))
46	35, 45	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (1...𝐵))
47	46	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (1...𝐵))
48	47	snssd 4805	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → {𝐵} ⊆ (1...𝐵))
49	44, 48	unssd 4182	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝐵))
50		simplr2 1216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)))
51		f1f 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ)
52	6, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹:(1...𝑁)⟶ℝ)
53	52	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐹:(1...𝑁)⟶ℝ)
54		elfzuz3 13480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ_≥‘𝐴))
55		fzss2 13523	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ (ℤ_≥‘𝐴) → (1...𝐴) ⊆ (1...𝑁))
56	4, 54, 55	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1...𝐴) ⊆ (1...𝑁))
57	56	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ⊆ (1...𝑁))
58	16, 57	sstrd 3988	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝑁))
59		fzssuz 13524	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
60		uzssz 12825	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℤ_≥‘1) ⊆ ℤ
61		zssre 12547	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℤ ⊆ ℝ
62	60, 61	sstri 3987	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℤ_≥‘1) ⊆ ℝ
63	59, 62	sstri 3987	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1...𝑁) ⊆ ℝ
64		ltso 11276	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ < Or ℝ
65		soss 5601	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (1...𝑁)))
66	63, 64, 65	mp2 9	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < Or (1...𝑁)
67		soisores 7308	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁))) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
68	66, 8, 67	mpanl12 700	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁)) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
69	53, 58, 68	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
70	50, 69	mpbid 231	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
71	70	r19.21bi 3247	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
72	16	sselda 3978	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ (1...𝐴))
73		elfzle2 13487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ (1...𝐴) → 𝑧 ≤ 𝐴)
74	72, 73	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ≤ 𝐴)
75	58	sselda 3978	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ (1...𝑁))
76	63, 75	sselid 3976	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ ℝ)
77	4	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ (1...𝑁))
78	77, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ ℕ)
79	78	nnred 12209	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ ℝ)
80	76, 79	lenltd 11342	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑧 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑧))
81	74, 80	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ¬ 𝐴 < 𝑧)
82	50	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)))
83		simplr3 1217	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐴 ∈ 𝑓)
84	83	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ 𝑓)
85		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ 𝑓)
86		isorel 7307	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (𝐴 < 𝑧 ↔ ((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧)))
87		fvres 6897	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ 𝑓 → ((𝐹 ↾ 𝑓)‘𝐴) = (𝐹‘𝐴))
88		fvres 6897	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 𝑓 → ((𝐹 ↾ 𝑓)‘𝑧) = (𝐹‘𝑧))
89	87, 88	breqan12d 5157	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓) → (((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧) ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
90	89	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧) ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
91	86, 90	bitrd 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (𝐴 < 𝑧 ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
92	82, 84, 85, 91	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐴 < 𝑧 ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
93	81, 92	mtbid 323	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧))
94		simplr 767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐴)𝑂(𝐹‘𝐵))
95	53	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐹:(1...𝑁)⟶ℝ)
96	95, 75	ffvelcdmd 7072	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝑧) ∈ ℝ)
97	95, 77	ffvelcdmd 7072	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐴) ∈ ℝ)
98	29	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (1...𝑁))
99	98	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐵 ∈ (1...𝑁))
100	95, 99	ffvelcdmd 7072	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐵) ∈ ℝ)
101		sotr2 5613	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑂 Or ℝ ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ)) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
102	8, 101	mpan 688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
103	96, 97, 100, 102	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
104	93, 94, 103	mp2and 697	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝑧)𝑂(𝐹‘𝐵))
105	104	a1d 25	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
106		elsni 4639	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ {𝐵} → 𝑤 = 𝐵)
107	106	fveq2d 6882	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ {𝐵} → (𝐹‘𝑤) = (𝐹‘𝐵))
108	107	breq2d 5153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ {𝐵} → ((𝐹‘𝑧)𝑂(𝐹‘𝑤) ↔ (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
109	108	imbi2d 340	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝐵))))
110	105, 109	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑤 ∈ {𝐵} → (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
111	110	ralrimiv 3144	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
112		ralunb 4187	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ∧ ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
113	71, 111, 112	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
114	113	ralrimiva 3145	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
115	49	sselda 3978	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → 𝑤 ∈ (1...𝐵))
116		elfzle2 13487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ≤ 𝐵)
117	116	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ≤ 𝐵)
118		elfzelz 13483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℤ)
119	118	zred 12648	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℝ)
120	119	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ∈ ℝ)
121	36	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝐵 ∈ ℝ)
122	120, 121	lenltd 11342	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → (𝑤 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑤))
123	117, 122	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → ¬ 𝐵 < 𝑤)
124	115, 123	syldan 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → ¬ 𝐵 < 𝑤)
125	124	pm2.21d 121	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → (𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
126	125	ralrimiva 3145	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
127		elsni 4639	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
128	127	breq1d 5151	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝐵} → (𝑧 < 𝑤 ↔ 𝐵 < 𝑤))
129	128	imbi1d 341	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
130	129	ralbidv 3176	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝐵} → (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
131	126, 130	syl5ibrcom 246	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑧 ∈ {𝐵} → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
132	131	ralrimiv 3144	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
133		ralunb 4187	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (∀𝑧 ∈ 𝑓 ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ∧ ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
134	114, 132, 133	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
135	98	snssd 4805	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → {𝐵} ⊆ (1...𝑁))
136	58, 135	unssd 4182	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))
137		soisores 7308	. . . . . . . . . . . . . . . . 17 ⊢ ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
138	66, 8, 137	mpanl12 700	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
139	53, 136, 138	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
140	134, 139	mpbird 256	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))))
141		ssun2 4169	. . . . . . . . . . . . . . 15 ⊢ {𝐵} ⊆ (𝑓 ∪ {𝐵})
142		snssg 4780	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝐵) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
143	47, 142	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
144	141, 143	mpbiri 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (𝑓 ∪ {𝐵}))
145	22	erdszelem1 34013	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} ↔ ((𝑓 ∪ {𝐵}) ⊆ (1...𝐵) ∧ (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ∧ 𝐵 ∈ (𝑓 ∪ {𝐵})))
146	49, 140, 144, 145	syl3anbrc 1343	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})
147		vex 3477	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
148		snex 5424	. . . . . . . . . . . . . . . 16 ⊢ {𝐵} ∈ V
149	147, 148	unex 7716	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∪ {𝐵}) ∈ V
150	1	fdmi 6716	. . . . . . . . . . . . . . 15 ⊢ dom ♯ = V
151	149, 150	eleqtrri 2831	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∪ {𝐵}) ∈ dom ♯
152		funfvima 7216	. . . . . . . . . . . . . 14 ⊢ ((Fun ♯ ∧ (𝑓 ∪ {𝐵}) ∈ dom ♯) → ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})))
153	3, 151, 152	mp2an 690	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
154	146, 153	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
155	154	ne0d 4331	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ≠ ∅)
156	23	simpli 484	. . . . . . . . . . . 12 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin
157		fimaxre2 12141	. . . . . . . . . . . 12 ⊢ (((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧)
158	27, 156, 157	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧)
159	33, 36	ltnled 11343	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
160	37, 159	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐵 ≤ 𝐴)
161		elfzle2 13487	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝐴) → 𝐵 ≤ 𝐴)
162	160, 161	nsyl 140	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝐵 ∈ (1...𝐴))
163	162	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ¬ 𝐵 ∈ (1...𝐴))
164	16, 163	ssneldd 3981	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ¬ 𝐵 ∈ 𝑓)
165		hashunsng 14334	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ (1...𝑁) → ((𝑓 ∈ Fin ∧ ¬ 𝐵 ∈ 𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
166	98, 165	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝑓 ∈ Fin ∧ ¬ 𝐵 ∈ 𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
167	18, 164, 166	mp2and 697	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1))
168	167, 154	eqeltrrd 2833	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
169		suprub 12157	. . . . . . . . . . 11 ⊢ ((((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧) ∧ ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
170	27, 155, 158, 168, 169	syl31anc 1373	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
171	5, 6, 7	erdszelem3 34015	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ (1...𝑁) → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
172	29, 171	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
173	172	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
174	170, 173	breqtrrd 5169	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵))
175	5, 6, 7, 8	erdszelem6 34018	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ)
176	175, 29	ffvelcdmd 7072	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾‘𝐵) ∈ ℕ)
177	176	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) ∈ ℕ)
178	177	nnnn0d 12514	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) ∈ ℕ₀)
179		nn0ltp1le 12602	. . . . . . . . . 10 ⊢ (((♯‘𝑓) ∈ ℕ₀ ∧ (𝐾‘𝐵) ∈ ℕ₀) → ((♯‘𝑓) < (𝐾‘𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵)))
180	20, 178, 179	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) < (𝐾‘𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵)))
181	174, 180	mpbird 256	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) < (𝐾‘𝐵))
182	21, 181	ltned 11332	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ≠ (𝐾‘𝐵))
183	182	ex 413	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (♯‘𝑓) ≠ (𝐾‘𝐵)))
184		neeq1 3002	. . . . . . 7 ⊢ ((♯‘𝑓) = (𝐾‘𝐴) → ((♯‘𝑓) ≠ (𝐾‘𝐵) ↔ (𝐾‘𝐴) ≠ (𝐾‘𝐵)))
185	184	imbi2d 340	. . . . . 6 ⊢ ((♯‘𝑓) = (𝐾‘𝐴) → (((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (♯‘𝑓) ≠ (𝐾‘𝐵)) ↔ ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
186	183, 185	syl5ibcom 244	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) → ((♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
187	14, 186	sylan2b 594	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) → ((♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
188	187	rexlimdva 3154	. . 3 ⊢ (𝜑 → (∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
189	12, 188	mpd 15	. 2 ⊢ (𝜑 → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵)))
190	189	necon2bd 2955	1 ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2939 ∀wral 3060 ∃wrex 3069 {crab 3431 Vcvv 3473 ∪ cun 3942 ⊆ wss 3944 ∅c0 4318 𝒫 cpw 4596 {csn 4622 class class class wbr 5141 ↦ cmpt 5224 Or wor 5580 dom cdm 5669 ↾ cres 5671 “ cima 5672 Fun wfun 6526 ⟶wf 6528 –1-1→wf1 6529 ‘cfv 6532 Isom wiso 6533 (class class class)co 7393 Fincfn 8922 supcsup 9417 ℝcr 11091 1c1 11093 + caddc 11095 +∞cpnf 11227 < clt 11230 ≤ cle 11231 ℕcn 12194 ℕ₀cn0 12454 ℤcz 12540 ℤ_≥cuz 12804 ...cfz 13466 ♯chash 14272

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7708 ax-cnex 11148 ax-resscn 11149 ax-1cn 11150 ax-icn 11151 ax-addcl 11152 ax-addrcl 11153 ax-mulcl 11154 ax-mulrcl 11155 ax-mulcom 11156 ax-addass 11157 ax-mulass 11158 ax-distr 11159 ax-i2m1 11160 ax-1ne0 11161 ax-1rid 11162 ax-rnegex 11163 ax-rrecex 11164 ax-cnre 11165 ax-pre-lttri 11166 ax-pre-lttrn 11167 ax-pre-ltadd 11168 ax-pre-mulgt0 11169 ax-pre-sup 11170

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3774 df-csb 3890 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3963 df-nul 4319 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-op 4629 df-uni 4902 df-int 4944 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6289 df-ord 6356 df-on 6357 df-lim 6358 df-suc 6359 df-iota 6484 df-fun 6534 df-fn 6535 df-f 6536 df-f1 6537 df-fo 6538 df-f1o 6539 df-fv 6540 df-isom 6541 df-riota 7349 df-ov 7396 df-oprab 7397 df-mpo 7398 df-om 7839 df-1st 7957 df-2nd 7958 df-frecs 8248 df-wrecs 8279 df-recs 8353 df-rdg 8392 df-1o 8448 df-oadd 8452 df-er 8686 df-en 8923 df-dom 8924 df-sdom 8925 df-fin 8926 df-sup 9419 df-dju 9878 df-card 9916 df-pnf 11232 df-mnf 11233 df-xr 11234 df-ltxr 11235 df-le 11236 df-sub 11428 df-neg 11429 df-nn 12195 df-n0 12455 df-xnn0 12527 df-z 12541 df-uz 12805 df-fz 13467 df-hash 14273

This theorem is referenced by: erdszelem9 34021

W3C validator