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 35441

Description: Lemma for erdsze 35445. (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 14295	. . . . 5 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
2		ffun 6662	. . . . 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 35438	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
10	4, 9	mpdan 694	. . . 4 ⊢ (𝜑 → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
11		fvelima 6896	. . . 4 ⊢ ((Fun ♯ ∧ (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})) → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴))
12	3, 10, 11	sylancr 594	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴))
13		eqid 2741	. . . . . 6 ⊢ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}
14	13	erdszelem1 35434	. . . . 5 ⊢ (𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} ↔ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓))
15		fzfid 13930	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ∈ Fin)
16		simplr1 1223	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝐴))
17		ssfi 9101	. . . . . . . . . . 11 ⊢ (((1...𝐴) ∈ Fin ∧ 𝑓 ⊆ (1...𝐴)) → 𝑓 ∈ Fin)
18	15, 16, 17	syl2anc 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ∈ Fin)
19		hashcl 14313	. . . . . . . . . 10 ⊢ (𝑓 ∈ Fin → (♯‘𝑓) ∈ ℕ₀)
20	18, 19	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ∈ ℕ₀)
21	20	nn0red 12494	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ∈ ℝ)
22		eqid 2741	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}
23	22	erdszelem2 35435	. . . . . . . . . . . . . 14 ⊢ ((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℕ)
24	23	simpri 487	. . . . . . . . . . . . 13 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℕ
25		nnssre 12173	. . . . . . . . . . . . 13 ⊢ ℕ ⊆ ℝ
26	24, 25	sstri 3926	. . . . . . . . . . . 12 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ
27	26	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ)
28	4	elfzelzd 13474	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℤ)
29		erdszelem.b	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (1...𝑁))
30	29	elfzelzd 13474	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ ℤ)
31		elfznn 13502	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ)
32	4, 31	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℕ)
33	32	nnred 12184	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℝ)
34		elfznn 13502	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℕ)
35	29, 34	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℕ)
36	35	nnred 12184	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℝ)
37		erdszelem.l	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 < 𝐵)
38	33, 36, 37	ltled 11289	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
39		eluz2 12789	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵))
40	28, 30, 38, 39	syl3anbrc 1351	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘𝐴))
41		fzss2 13513	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (1...𝐴) ⊆ (1...𝐵))
42	40, 41	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝐴) ⊆ (1...𝐵))
43	42	ad2antrr 733	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ⊆ (1...𝐵))
44	16, 43	sstrd 3927	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝐵))
45		elfz1end 13503	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵))
46	35, 45	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (1...𝐵))
47	46	ad2antrr 733	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (1...𝐵))
48	47	snssd 4721	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → {𝐵} ⊆ (1...𝐵))
49	44, 48	unssd 4124	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝐵))
50		simplr2 1224	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)))
51		f1f 6727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ)
52	6, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹:(1...𝑁)⟶ℝ)
53	52	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐹:(1...𝑁)⟶ℝ)
54		elfzuz3 13470	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ_≥‘𝐴))
55		fzss2 13513	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ (ℤ_≥‘𝐴) → (1...𝐴) ⊆ (1...𝑁))
56	4, 54, 55	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1...𝐴) ⊆ (1...𝑁))
57	56	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ⊆ (1...𝑁))
58	16, 57	sstrd 3927	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝑁))
59		fzssuz 13514	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
60		uzssz 12804	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℤ_≥‘1) ⊆ ℤ
61		zssre 12526	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℤ ⊆ ℝ
62	60, 61	sstri 3926	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℤ_≥‘1) ⊆ ℝ
63	59, 62	sstri 3926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1...𝑁) ⊆ ℝ
64		ltso 11221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ < Or ℝ
65		soss 5549	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (1...𝑁)))
66	63, 64, 65	mp2 9	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < Or (1...𝑁)
67		soisores 7275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁))) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
68	66, 8, 67	mpanl12 709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁)) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
69	53, 58, 68	syl2anc 591	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
70	50, 69	mpbid 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
71	70	r19.21bi 3233	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
72	16	sselda 3917	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ (1...𝐴))
73		elfzle2 13477	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ (1...𝐴) → 𝑧 ≤ 𝐴)
74	72, 73	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ≤ 𝐴)
75	58	sselda 3917	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ (1...𝑁))
76	63, 75	sselid 3915	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ ℝ)
77	4	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ (1...𝑁))
78	77, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ ℕ)
79	78	nnred 12184	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ ℝ)
80	76, 79	lenltd 11287	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑧 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑧))
81	74, 80	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ¬ 𝐴 < 𝑧)
82	50	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)))
83		simplr3 1225	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐴 ∈ 𝑓)
84	83	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ 𝑓)
85		simpr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ 𝑓)
86		isorel 7274	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (𝐴 < 𝑧 ↔ ((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧)))
87		fvres 6850	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ 𝑓 → ((𝐹 ↾ 𝑓)‘𝐴) = (𝐹‘𝐴))
88		fvres 6850	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 𝑓 → ((𝐹 ↾ 𝑓)‘𝑧) = (𝐹‘𝑧))
89	87, 88	breqan12d 5091	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓) → (((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧) ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
90	89	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧) ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
91	86, 90	bitrd 281	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (𝐴 < 𝑧 ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
92	82, 84, 85, 91	syl12anc 843	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐴 < 𝑧 ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
93	81, 92	mtbid 326	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧))
94		simplr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐴)𝑂(𝐹‘𝐵))
95	53	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐹:(1...𝑁)⟶ℝ)
96	95, 75	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝑧) ∈ ℝ)
97	95, 77	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐴) ∈ ℝ)
98	29	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (1...𝑁))
99	98	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐵 ∈ (1...𝑁))
100	95, 99	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐵) ∈ ℝ)
101		sotr2 5563	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑂 Or ℝ ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ)) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
102	8, 101	mpan 697	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
103	96, 97, 100, 102	syl3anc 1380	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
104	93, 94, 103	mp2and 706	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝑧)𝑂(𝐹‘𝐵))
105	104	a1d 25	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
106		elsni 4575	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ {𝐵} → 𝑤 = 𝐵)
107	106	fveq2d 6835	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ {𝐵} → (𝐹‘𝑤) = (𝐹‘𝐵))
108	107	breq2d 5087	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ {𝐵} → ((𝐹‘𝑧)𝑂(𝐹‘𝑤) ↔ (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
109	108	imbi2d 342	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝐵))))
110	105, 109	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑤 ∈ {𝐵} → (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
111	110	ralrimiv 3132	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
112		ralunb 4129	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ∧ ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
113	71, 111, 112	sylanbrc 590	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
114	113	ralrimiva 3133	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
115	49	sselda 3917	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → 𝑤 ∈ (1...𝐵))
116		elfzle2 13477	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ≤ 𝐵)
117	116	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ≤ 𝐵)
118		elfzelz 13473	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℤ)
119	118	zred 12628	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℝ)
120	119	adantl 483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ∈ ℝ)
121	36	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝐵 ∈ ℝ)
122	120, 121	lenltd 11287	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → (𝑤 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑤))
123	117, 122	mpbid 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → ¬ 𝐵 < 𝑤)
124	115, 123	syldan 598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → ¬ 𝐵 < 𝑤)
125	124	pm2.21d 121	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → (𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
126	125	ralrimiva 3133	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
127		elsni 4575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
128	127	breq1d 5085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝐵} → (𝑧 < 𝑤 ↔ 𝐵 < 𝑤))
129	128	imbi1d 343	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
130	129	ralbidv 3164	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝐵} → (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
131	126, 130	syl5ibrcom 249	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑧 ∈ {𝐵} → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
132	131	ralrimiv 3132	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
133		ralunb 4129	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (∀𝑧 ∈ 𝑓 ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ∧ ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
134	114, 132, 133	sylanbrc 590	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
135	98	snssd 4721	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → {𝐵} ⊆ (1...𝑁))
136	58, 135	unssd 4124	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))
137		soisores 7275	. . . . . . . . . . . . . . . . 17 ⊢ ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
138	66, 8, 137	mpanl12 709	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
139	53, 136, 138	syl2anc 591	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
140	134, 139	mpbird 259	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))))
141		ssun2 4111	. . . . . . . . . . . . . . 15 ⊢ {𝐵} ⊆ (𝑓 ∪ {𝐵})
142		snssg 4718	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝐵) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
143	47, 142	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
144	141, 143	mpbiri 260	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (𝑓 ∪ {𝐵}))
145	22	erdszelem1 35434	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} ↔ ((𝑓 ∪ {𝐵}) ⊆ (1...𝐵) ∧ (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ∧ 𝐵 ∈ (𝑓 ∪ {𝐵})))
146	49, 140, 144, 145	syl3anbrc 1351	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})
147		vex 3437	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
148		snex 5371	. . . . . . . . . . . . . . . 16 ⊢ {𝐵} ∈ V
149	147, 148	unex 7691	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∪ {𝐵}) ∈ V
150	1	fdmi 6670	. . . . . . . . . . . . . . 15 ⊢ dom ♯ = V
151	149, 150	eleqtrri 2840	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∪ {𝐵}) ∈ dom ♯
152		funfvima 7178	. . . . . . . . . . . . . 14 ⊢ ((Fun ♯ ∧ (𝑓 ∪ {𝐵}) ∈ dom ♯) → ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})))
153	3, 151, 152	mp2an 699	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
154	146, 153	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
155	154	ne0d 4273	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ≠ ∅)
156	23	simpli 485	. . . . . . . . . . . 12 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin
157		fimaxre2 12096	. . . . . . . . . . . 12 ⊢ (((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧)
158	27, 156, 157	sylancl 593	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧)
159	33, 36	ltnled 11288	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
160	37, 159	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐵 ≤ 𝐴)
161		elfzle2 13477	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝐴) → 𝐵 ≤ 𝐴)
162	160, 161	nsyl 140	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝐵 ∈ (1...𝐴))
163	162	ad2antrr 733	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ¬ 𝐵 ∈ (1...𝐴))
164	16, 163	ssneldd 3920	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ¬ 𝐵 ∈ 𝑓)
165		hashunsng 14349	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ (1...𝑁) → ((𝑓 ∈ Fin ∧ ¬ 𝐵 ∈ 𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
166	98, 165	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝑓 ∈ Fin ∧ ¬ 𝐵 ∈ 𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
167	18, 164, 166	mp2and 706	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1))
168	167, 154	eqeltrrd 2842	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
169		suprub 12112	. . . . . . . . . . 11 ⊢ ((((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧) ∧ ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
170	27, 155, 158, 168, 169	syl31anc 1382	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
171	5, 6, 7	erdszelem3 35436	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ (1...𝑁) → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
172	29, 171	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
173	172	ad2antrr 733	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
174	170, 173	breqtrrd 5103	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵))
175	5, 6, 7, 8	erdszelem6 35439	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ)
176	175, 29	ffvelcdmd 7030	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾‘𝐵) ∈ ℕ)
177	176	ad2antrr 733	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) ∈ ℕ)
178	177	nnnn0d 12493	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) ∈ ℕ₀)
179		nn0ltp1le 12582	. . . . . . . . . 10 ⊢ (((♯‘𝑓) ∈ ℕ₀ ∧ (𝐾‘𝐵) ∈ ℕ₀) → ((♯‘𝑓) < (𝐾‘𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵)))
180	20, 178, 179	syl2anc 591	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) < (𝐾‘𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵)))
181	174, 180	mpbird 259	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) < (𝐾‘𝐵))
182	21, 181	ltned 11277	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ≠ (𝐾‘𝐵))
183	182	ex 414	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (♯‘𝑓) ≠ (𝐾‘𝐵)))
184		neeq1 2998	. . . . . . 7 ⊢ ((♯‘𝑓) = (𝐾‘𝐴) → ((♯‘𝑓) ≠ (𝐾‘𝐵) ↔ (𝐾‘𝐴) ≠ (𝐾‘𝐵)))
185	184	imbi2d 342	. . . . . 6 ⊢ ((♯‘𝑓) = (𝐾‘𝐴) → (((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (♯‘𝑓) ≠ (𝐾‘𝐵)) ↔ ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
186	183, 185	syl5ibcom 247	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) → ((♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
187	14, 186	sylan2b 601	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) → ((♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
188	187	rexlimdva 3142	. . 3 ⊢ (𝜑 → (∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
189	12, 188	mpd 15	. 2 ⊢ (𝜑 → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵)))
190	189	necon2bd 2952	1 ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 397 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 ∀wral 3055 ∃wrex 3065 {crab 3393 Vcvv 3433 ∪ cun 3883 ⊆ wss 3885 ∅c0 4264 𝒫 cpw 4532 {csn 4558 class class class wbr 5075 ↦ cmpt 5156 Or wor 5528 dom cdm 5621 ↾ cres 5623 “ cima 5624 Fun wfun 6483 ⟶wf 6485 –1-1→wf1 6486 ‘cfv 6489 Isom wiso 6490 (class class class)co 7360 Fincfn 8887 supcsup 9347 ℝcr 11032 1c1 11034 + caddc 11036 +∞cpnf 11171 < clt 11174 ≤ cle 11175 ℕcn 12169 ℕ₀cn0 12432 ℤcz 12519 ℤ_≥cuz 12783 ...cfz 13456 ♯chash 14287

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-int 4881 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-isom 6498 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-oadd 8403 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-sup 9349 df-dju 9820 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-nn 12170 df-n0 12433 df-xnn0 12506 df-z 12520 df-uz 12784 df-fz 13457 df-hash 14288

This theorem is referenced by: erdszelem9 35442

W3C validator