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 34177

Description: Lemma for erdsze 34181. (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 14294	. . . . 5 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
2		ffun 6717	. . . . 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 34174	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
10	4, 9	mpdan 685	. . . 4 ⊢ (𝜑 → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
11		fvelima 6954	. . . 4 ⊢ ((Fun ♯ ∧ (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})) → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴))
12	3, 10, 11	sylancr 587	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴))
13		eqid 2732	. . . . . 6 ⊢ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}
14	13	erdszelem1 34170	. . . . 5 ⊢ (𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} ↔ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓))
15		fzfid 13934	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ∈ Fin)
16		simplr1 1215	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝐴))
17		ssfi 9169	. . . . . . . . . . 11 ⊢ (((1...𝐴) ∈ Fin ∧ 𝑓 ⊆ (1...𝐴)) → 𝑓 ∈ Fin)
18	15, 16, 17	syl2anc 584	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ∈ Fin)
19		hashcl 14312	. . . . . . . . . 10 ⊢ (𝑓 ∈ Fin → (♯‘𝑓) ∈ ℕ₀)
20	18, 19	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ∈ ℕ₀)
21	20	nn0red 12529	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ∈ ℝ)
22		eqid 2732	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}
23	22	erdszelem2 34171	. . . . . . . . . . . . . 14 ⊢ ((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℕ)
24	23	simpri 486	. . . . . . . . . . . . 13 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℕ
25		nnssre 12212	. . . . . . . . . . . . 13 ⊢ ℕ ⊆ ℝ
26	24, 25	sstri 3990	. . . . . . . . . . . 12 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ
27	26	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ)
28	4	elfzelzd 13498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℤ)
29		erdszelem.b	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (1...𝑁))
30	29	elfzelzd 13498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ ℤ)
31		elfznn 13526	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ)
32	4, 31	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℕ)
33	32	nnred 12223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℝ)
34		elfznn 13526	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℕ)
35	29, 34	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℕ)
36	35	nnred 12223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℝ)
37		erdszelem.l	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 < 𝐵)
38	33, 36, 37	ltled 11358	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
39		eluz2 12824	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵))
40	28, 30, 38, 39	syl3anbrc 1343	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘𝐴))
41		fzss2 13537	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (1...𝐴) ⊆ (1...𝐵))
42	40, 41	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝐴) ⊆ (1...𝐵))
43	42	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ⊆ (1...𝐵))
44	16, 43	sstrd 3991	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝐵))
45		elfz1end 13527	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵))
46	35, 45	sylib 217	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (1...𝐵))
47	46	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (1...𝐵))
48	47	snssd 4811	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → {𝐵} ⊆ (1...𝐵))
49	44, 48	unssd 4185	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝐵))
50		simplr2 1216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)))
51		f1f 6784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ)
52	6, 51	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹:(1...𝑁)⟶ℝ)
53	52	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐹:(1...𝑁)⟶ℝ)
54		elfzuz3 13494	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ_≥‘𝐴))
55		fzss2 13537	. . . . . . . . . . . . . . . . . . . . . . . 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 3991	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝑁))
59		fzssuz 13538	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
60		uzssz 12839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℤ_≥‘1) ⊆ ℤ
61		zssre 12561	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℤ ⊆ ℝ
62	60, 61	sstri 3990	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℤ_≥‘1) ⊆ ℝ
63	59, 62	sstri 3990	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1...𝑁) ⊆ ℝ
64		ltso 11290	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ < Or ℝ
65		soss 5607	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (1...𝑁)))
66	63, 64, 65	mp2 9	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < Or (1...𝑁)
67		soisores 7320	. . . . . . . . . . . . . . . . . . . . . 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 3248	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
72	16	sselda 3981	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ (1...𝐴))
73		elfzle2 13501	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ (1...𝐴) → 𝑧 ≤ 𝐴)
74	72, 73	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ≤ 𝐴)
75	58	sselda 3981	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ (1...𝑁))
76	63, 75	sselid 3979	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ ℝ)
77	4	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ (1...𝑁))
78	77, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ ℕ)
79	78	nnred 12223	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ ℝ)
80	76, 79	lenltd 11356	. . . . . . . . . . . . . . . . . . . . . . . 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 7319	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (𝐴 < 𝑧 ↔ ((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧)))
87		fvres 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ 𝑓 → ((𝐹 ↾ 𝑓)‘𝐴) = (𝐹‘𝐴))
88		fvres 6907	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 𝑓 → ((𝐹 ↾ 𝑓)‘𝑧) = (𝐹‘𝑧))
89	87, 88	breqan12d 5163	. . . . . . . . . . . . . . . . . . . . . . . . . 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 7084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝑧) ∈ ℝ)
97	95, 77	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐴) ∈ ℝ)
98	29	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (1...𝑁))
99	98	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐵 ∈ (1...𝑁))
100	95, 99	ffvelcdmd 7084	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐵) ∈ ℝ)
101		sotr2 5619	. . . . . . . . . . . . . . . . . . . . . . . 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 4644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ {𝐵} → 𝑤 = 𝐵)
107	106	fveq2d 6892	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ {𝐵} → (𝐹‘𝑤) = (𝐹‘𝐵))
108	107	breq2d 5159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ {𝐵} → ((𝐹‘𝑧)𝑂(𝐹‘𝑤) ↔ (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
109	108	imbi2d 340	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝐵))))
110	105, 109	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑤 ∈ {𝐵} → (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
111	110	ralrimiv 3145	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
112		ralunb 4190	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ∧ ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
113	71, 111, 112	sylanbrc 583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
114	113	ralrimiva 3146	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
115	49	sselda 3981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → 𝑤 ∈ (1...𝐵))
116		elfzle2 13501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ≤ 𝐵)
117	116	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ≤ 𝐵)
118		elfzelz 13497	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℤ)
119	118	zred 12662	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℝ)
120	119	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ∈ ℝ)
121	36	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝐵 ∈ ℝ)
122	120, 121	lenltd 11356	. . . . . . . . . . . . . . . . . . . . . 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 3146	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
127		elsni 4644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
128	127	breq1d 5157	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝐵} → (𝑧 < 𝑤 ↔ 𝐵 < 𝑤))
129	128	imbi1d 341	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
130	129	ralbidv 3177	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝐵} → (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
131	126, 130	syl5ibrcom 246	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑧 ∈ {𝐵} → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
132	131	ralrimiv 3145	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
133		ralunb 4190	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (∀𝑧 ∈ 𝑓 ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ∧ ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
134	114, 132, 133	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
135	98	snssd 4811	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → {𝐵} ⊆ (1...𝑁))
136	58, 135	unssd 4185	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))
137		soisores 7320	. . . . . . . . . . . . . . . . 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 4172	. . . . . . . . . . . . . . 15 ⊢ {𝐵} ⊆ (𝑓 ∪ {𝐵})
142		snssg 4786	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝐵) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
143	47, 142	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
144	141, 143	mpbiri 257	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (𝑓 ∪ {𝐵}))
145	22	erdszelem1 34170	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} ↔ ((𝑓 ∪ {𝐵}) ⊆ (1...𝐵) ∧ (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ∧ 𝐵 ∈ (𝑓 ∪ {𝐵})))
146	49, 140, 144, 145	syl3anbrc 1343	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})
147		vex 3478	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
148		snex 5430	. . . . . . . . . . . . . . . 16 ⊢ {𝐵} ∈ V
149	147, 148	unex 7729	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∪ {𝐵}) ∈ V
150	1	fdmi 6726	. . . . . . . . . . . . . . 15 ⊢ dom ♯ = V
151	149, 150	eleqtrri 2832	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∪ {𝐵}) ∈ dom ♯
152		funfvima 7228	. . . . . . . . . . . . . 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 4334	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ≠ ∅)
156	23	simpli 484	. . . . . . . . . . . 12 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin
157		fimaxre2 12155	. . . . . . . . . . . 12 ⊢ (((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧)
158	27, 156, 157	sylancl 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧)
159	33, 36	ltnled 11357	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
160	37, 159	mpbid 231	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐵 ≤ 𝐴)
161		elfzle2 13501	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝐴) → 𝐵 ≤ 𝐴)
162	160, 161	nsyl 140	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝐵 ∈ (1...𝐴))
163	162	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ¬ 𝐵 ∈ (1...𝐴))
164	16, 163	ssneldd 3984	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ¬ 𝐵 ∈ 𝑓)
165		hashunsng 14348	. . . . . . . . . . . . . 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 2834	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
169		suprub 12171	. . . . . . . . . . 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 34172	. . . . . . . . . . . 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 5175	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵))
175	5, 6, 7, 8	erdszelem6 34175	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ)
176	175, 29	ffvelcdmd 7084	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾‘𝐵) ∈ ℕ)
177	176	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) ∈ ℕ)
178	177	nnnn0d 12528	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) ∈ ℕ₀)
179		nn0ltp1le 12616	. . . . . . . . . 10 ⊢ (((♯‘𝑓) ∈ ℕ₀ ∧ (𝐾‘𝐵) ∈ ℕ₀) → ((♯‘𝑓) < (𝐾‘𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵)))
180	20, 178, 179	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) < (𝐾‘𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵)))
181	174, 180	mpbird 256	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) < (𝐾‘𝐵))
182	21, 181	ltned 11346	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ≠ (𝐾‘𝐵))
183	182	ex 413	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (♯‘𝑓) ≠ (𝐾‘𝐵)))
184		neeq1 3003	. . . . . . 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 3155	. . 3 ⊢ (𝜑 → (∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
189	12, 188	mpd 15	. 2 ⊢ (𝜑 → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵)))
190	189	necon2bd 2956	1 ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3432 Vcvv 3474 ∪ cun 3945 ⊆ wss 3947 ∅c0 4321 𝒫 cpw 4601 {csn 4627 class class class wbr 5147 ↦ cmpt 5230 Or wor 5586 dom cdm 5675 ↾ cres 5677 “ cima 5678 Fun wfun 6534 ⟶wf 6536 –1-1→wf1 6537 ‘cfv 6540 Isom wiso 6541 (class class class)co 7405 Fincfn 8935 supcsup 9431 ℝcr 11105 1c1 11107 + caddc 11109 +∞cpnf 11241 < clt 11244 ≤ cle 11245 ℕcn 12208 ℕ₀cn0 12468 ℤcz 12554 ℤ_≥cuz 12818 ...cfz 13480 ♯chash 14286

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 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

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 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3376 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6297 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7852 df-1st 7971 df-2nd 7972 df-frecs 8262 df-wrecs 8293 df-recs 8367 df-rdg 8406 df-1o 8462 df-oadd 8466 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-fin 8939 df-sup 9433 df-dju 9892 df-card 9930 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11442 df-neg 11443 df-nn 12209 df-n0 12469 df-xnn0 12541 df-z 12555 df-uz 12819 df-fz 13481 df-hash 14287

This theorem is referenced by: erdszelem9 34178

W3C validator