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 32440

Description: Lemma for erdsze 32444. (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 13692	. . . . 5 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
2		ffun 6511	. . . . 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 32437	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
10	4, 9	mpdan 685	. . . 4 ⊢ (𝜑 → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
11		fvelima 6725	. . . 4 ⊢ ((Fun ♯ ∧ (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})) → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴))
12	3, 10, 11	sylancr 589	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴))
13		eqid 2821	. . . . . 6 ⊢ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}
14	13	erdszelem1 32433	. . . . 5 ⊢ (𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} ↔ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓))
15		fzfid 13335	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ∈ Fin)
16		simplr1 1211	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝐴))
17		ssfi 8732	. . . . . . . . . . 11 ⊢ (((1...𝐴) ∈ Fin ∧ 𝑓 ⊆ (1...𝐴)) → 𝑓 ∈ Fin)
18	15, 16, 17	syl2anc 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ∈ Fin)
19		hashcl 13711	. . . . . . . . . 10 ⊢ (𝑓 ∈ Fin → (♯‘𝑓) ∈ ℕ₀)
20	18, 19	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ∈ ℕ₀)
21	20	nn0red 11950	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ∈ ℝ)
22		eqid 2821	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}
23	22	erdszelem2 32434	. . . . . . . . . . . . . 14 ⊢ ((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℕ)
24	23	simpri 488	. . . . . . . . . . . . 13 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℕ
25		nnssre 11636	. . . . . . . . . . . . 13 ⊢ ℕ ⊆ ℝ
26	24, 25	sstri 3975	. . . . . . . . . . . 12 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ
27	26	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ)
28		elfzelz 12902	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℤ)
29	4, 28	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℤ)
30		erdszelem.b	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ (1...𝑁))
31		elfzelz 12902	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℤ)
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ ℤ)
33		elfznn 12930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ)
34	4, 33	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐴 ∈ ℕ)
35	34	nnred 11647	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℝ)
36		elfznn 12930	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℕ)
37	30, 36	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ ℕ)
38	37	nnred 11647	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℝ)
39		erdszelem.l	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 < 𝐵)
40	35, 38, 39	ltled 10782	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
41		eluz2 12243	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵))
42	29, 32, 40, 41	syl3anbrc 1339	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘𝐴))
43		fzss2 12941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (1...𝐴) ⊆ (1...𝐵))
44	42, 43	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (1...𝐴) ⊆ (1...𝐵))
45	44	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ⊆ (1...𝐵))
46	16, 45	sstrd 3976	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝐵))
47		elfz1end 12931	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵))
48	37, 47	sylib 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐵 ∈ (1...𝐵))
49	48	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (1...𝐵))
50	49	snssd 4735	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → {𝐵} ⊆ (1...𝐵))
51	46, 50	unssd 4161	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝐵))
52		simplr2 1212	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)))
53		f1f 6569	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ)
54	6, 53	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹:(1...𝑁)⟶ℝ)
55	54	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐹:(1...𝑁)⟶ℝ)
56		elfzuz3 12899	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ_≥‘𝐴))
57		fzss2 12941	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁 ∈ (ℤ_≥‘𝐴) → (1...𝐴) ⊆ (1...𝑁))
58	4, 56, 57	3syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → (1...𝐴) ⊆ (1...𝑁))
59	58	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ⊆ (1...𝑁))
60	16, 59	sstrd 3976	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝑁))
61		fzssuz 12942	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
62		uzssz 12258	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℤ_≥‘1) ⊆ ℤ
63		zssre 11982	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ℤ ⊆ ℝ
64	62, 63	sstri 3975	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℤ_≥‘1) ⊆ ℝ
65	61, 64	sstri 3975	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (1...𝑁) ⊆ ℝ
66		ltso 10715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ < Or ℝ
67		soss 5487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((1...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (1...𝑁)))
68	65, 66, 67	mp2 9	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ < Or (1...𝑁)
69		soisores 7074	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁))) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
70	68, 8, 69	mpanl12 700	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁)) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
71	55, 60, 70	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
72	52, 71	mpbid 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
73	72	r19.21bi 3208	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
74	16	sselda 3966	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ (1...𝐴))
75		elfzle2 12905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑧 ∈ (1...𝐴) → 𝑧 ≤ 𝐴)
76	74, 75	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ≤ 𝐴)
77	60	sselda 3966	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ (1...𝑁))
78	65, 77	sseldi 3964	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ ℝ)
79	4	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ (1...𝑁))
80	79, 33	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ ℕ)
81	80	nnred 11647	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ ℝ)
82	78, 81	lenltd 10780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑧 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑧))
83	76, 82	mpbid 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ¬ 𝐴 < 𝑧)
84	52	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)))
85		simplr3 1213	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐴 ∈ 𝑓)
86	85	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ 𝑓)
87		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ 𝑓)
88		isorel 7073	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (𝐴 < 𝑧 ↔ ((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧)))
89		fvres 6683	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝐴 ∈ 𝑓 → ((𝐹 ↾ 𝑓)‘𝐴) = (𝐹‘𝐴))
90		fvres 6683	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑧 ∈ 𝑓 → ((𝐹 ↾ 𝑓)‘𝑧) = (𝐹‘𝑧))
91	89, 90	breqan12d 5074	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓) → (((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧) ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
92	91	adantl 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧) ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
93	88, 92	bitrd 281	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (𝐴 < 𝑧 ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
94	84, 86, 87, 93	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐴 < 𝑧 ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
95	83, 94	mtbid 326	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧))
96		simplr 767	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐴)𝑂(𝐹‘𝐵))
97	55	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐹:(1...𝑁)⟶ℝ)
98	97, 77	ffvelrnd 6846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝑧) ∈ ℝ)
99	97, 79	ffvelrnd 6846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐴) ∈ ℝ)
100	30	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (1...𝑁))
101	100	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐵 ∈ (1...𝑁))
102	97, 101	ffvelrnd 6846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐵) ∈ ℝ)
103		sotr2 5499	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑂 Or ℝ ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ)) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
104	8, 103	mpan 688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
105	98, 99, 102, 104	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
106	95, 96, 105	mp2and 697	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝑧)𝑂(𝐹‘𝐵))
107	106	a1d 25	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
108		elsni 4577	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ {𝐵} → 𝑤 = 𝐵)
109	108	fveq2d 6668	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ {𝐵} → (𝐹‘𝑤) = (𝐹‘𝐵))
110	109	breq2d 5070	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ {𝐵} → ((𝐹‘𝑧)𝑂(𝐹‘𝑤) ↔ (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
111	110	imbi2d 343	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝐵))))
112	107, 111	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑤 ∈ {𝐵} → (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
113	112	ralrimiv 3181	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
114		ralunb 4166	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ∧ ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
115	73, 113, 114	sylanbrc 585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
116	115	ralrimiva 3182	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
117	51	sselda 3966	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → 𝑤 ∈ (1...𝐵))
118		elfzle2 12905	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ≤ 𝐵)
119	118	adantl 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ≤ 𝐵)
120		elfzelz 12902	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℤ)
121	120	zred 12081	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℝ)
122	121	adantl 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ∈ ℝ)
123	38	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝐵 ∈ ℝ)
124	122, 123	lenltd 10780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → (𝑤 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑤))
125	119, 124	mpbid 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → ¬ 𝐵 < 𝑤)
126	117, 125	syldan 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → ¬ 𝐵 < 𝑤)
127	126	pm2.21d 121	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → (𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
128	127	ralrimiva 3182	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
129		elsni 4577	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
130	129	breq1d 5068	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝐵} → (𝑧 < 𝑤 ↔ 𝐵 < 𝑤))
131	130	imbi1d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
132	131	ralbidv 3197	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ {𝐵} → (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
133	128, 132	syl5ibrcom 249	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑧 ∈ {𝐵} → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
134	133	ralrimiv 3181	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
135		ralunb 4166	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (∀𝑧 ∈ 𝑓 ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ∧ ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
136	116, 134, 135	sylanbrc 585	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
137	100	snssd 4735	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → {𝐵} ⊆ (1...𝑁))
138	60, 137	unssd 4161	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))
139		soisores 7074	. . . . . . . . . . . . . . . . 17 ⊢ ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
140	68, 8, 139	mpanl12 700	. . . . . . . . . . . . . . . 16 ⊢ ((𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
141	55, 138, 140	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
142	136, 141	mpbird 259	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))))
143		ssun2 4148	. . . . . . . . . . . . . . 15 ⊢ {𝐵} ⊆ (𝑓 ∪ {𝐵})
144		snssg 4710	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝐵) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
145	49, 144	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
146	143, 145	mpbiri 260	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (𝑓 ∪ {𝐵}))
147	22	erdszelem1 32433	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} ↔ ((𝑓 ∪ {𝐵}) ⊆ (1...𝐵) ∧ (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ∧ 𝐵 ∈ (𝑓 ∪ {𝐵})))
148	51, 142, 146, 147	syl3anbrc 1339	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})
149		vex 3497	. . . . . . . . . . . . . . . 16 ⊢ 𝑓 ∈ V
150		snex 5323	. . . . . . . . . . . . . . . 16 ⊢ {𝐵} ∈ V
151	149, 150	unex 7463	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∪ {𝐵}) ∈ V
152	1	fdmi 6518	. . . . . . . . . . . . . . 15 ⊢ dom ♯ = V
153	151, 152	eleqtrri 2912	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∪ {𝐵}) ∈ dom ♯
154		funfvima 6986	. . . . . . . . . . . . . 14 ⊢ ((Fun ♯ ∧ (𝑓 ∪ {𝐵}) ∈ dom ♯) → ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})))
155	3, 153, 154	mp2an 690	. . . . . . . . . . . . 13 ⊢ ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
156	148, 155	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
157	156	ne0d 4300	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ≠ ∅)
158	23	simpli 486	. . . . . . . . . . . 12 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin
159		fimaxre2 11580	. . . . . . . . . . . 12 ⊢ (((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧)
160	27, 158, 159	sylancl 588	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧)
161	35, 38	ltnled 10781	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
162	39, 161	mpbid 234	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐵 ≤ 𝐴)
163		elfzle2 12905	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ (1...𝐴) → 𝐵 ≤ 𝐴)
164	162, 163	nsyl 142	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ¬ 𝐵 ∈ (1...𝐴))
165	164	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ¬ 𝐵 ∈ (1...𝐴))
166	16, 165	ssneldd 3969	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ¬ 𝐵 ∈ 𝑓)
167		hashunsng 13747	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ (1...𝑁) → ((𝑓 ∈ Fin ∧ ¬ 𝐵 ∈ 𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
168	100, 167	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝑓 ∈ Fin ∧ ¬ 𝐵 ∈ 𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
169	18, 166, 168	mp2and 697	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1))
170	169, 156	eqeltrrd 2914	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
171		suprub 11596	. . . . . . . . . . 11 ⊢ ((((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧) ∧ ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
172	27, 157, 160, 170, 171	syl31anc 1369	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
173	5, 6, 7	erdszelem3 32435	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ (1...𝑁) → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
174	30, 173	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
175	174	ad2antrr 724	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
176	172, 175	breqtrrd 5086	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵))
177	5, 6, 7, 8	erdszelem6 32438	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ)
178	177, 30	ffvelrnd 6846	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾‘𝐵) ∈ ℕ)
179	178	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) ∈ ℕ)
180	179	nnnn0d 11949	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) ∈ ℕ₀)
181		nn0ltp1le 12034	. . . . . . . . . 10 ⊢ (((♯‘𝑓) ∈ ℕ₀ ∧ (𝐾‘𝐵) ∈ ℕ₀) → ((♯‘𝑓) < (𝐾‘𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵)))
182	20, 180, 181	syl2anc 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) < (𝐾‘𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵)))
183	176, 182	mpbird 259	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) < (𝐾‘𝐵))
184	21, 183	ltned 10770	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ≠ (𝐾‘𝐵))
185	184	ex 415	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (♯‘𝑓) ≠ (𝐾‘𝐵)))
186		neeq1 3078	. . . . . . 7 ⊢ ((♯‘𝑓) = (𝐾‘𝐴) → ((♯‘𝑓) ≠ (𝐾‘𝐵) ↔ (𝐾‘𝐴) ≠ (𝐾‘𝐵)))
187	186	imbi2d 343	. . . . . 6 ⊢ ((♯‘𝑓) = (𝐾‘𝐴) → (((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (♯‘𝑓) ≠ (𝐾‘𝐵)) ↔ ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
188	185, 187	syl5ibcom 247	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) → ((♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
189	14, 188	sylan2b 595	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) → ((♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
190	189	rexlimdva 3284	. . 3 ⊢ (𝜑 → (∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
191	12, 190	mpd 15	. 2 ⊢ (𝜑 → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵)))
192	191	necon2bd 3032	1 ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 {crab 3142 Vcvv 3494 ∪ cun 3933 ⊆ wss 3935 ∅c0 4290 𝒫 cpw 4538 {csn 4560 class class class wbr 5058 ↦ cmpt 5138 Or wor 5467 dom cdm 5549 ↾ cres 5551 “ cima 5552 Fun wfun 6343 ⟶wf 6345 –1-1→wf1 6346 ‘cfv 6349 Isom wiso 6350 (class class class)co 7150 Fincfn 8503 supcsup 8898 ℝcr 10530 1c1 10532 + caddc 10534 +∞cpnf 10666 < clt 10669 ≤ cle 10670 ℕcn 11632 ℕ₀cn0 11891 ℤcz 11975 ℤ_≥cuz 12237 ...cfz 12886 ♯chash 13684

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-rep 5182 ax-sep 5195 ax-nul 5202 ax-pow 5258 ax-pr 5321 ax-un 7455 ax-cnex 10587 ax-resscn 10588 ax-1cn 10589 ax-icn 10590 ax-addcl 10591 ax-addrcl 10592 ax-mulcl 10593 ax-mulrcl 10594 ax-mulcom 10595 ax-addass 10596 ax-mulass 10597 ax-distr 10598 ax-i2m1 10599 ax-1ne0 10600 ax-1rid 10601 ax-rnegex 10602 ax-rrecex 10603 ax-cnre 10604 ax-pre-lttri 10605 ax-pre-lttrn 10606 ax-pre-ltadd 10607 ax-pre-mulgt0 10608 ax-pre-sup 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3772 df-csb 3883 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4561 df-pr 4563 df-tp 4565 df-op 4567 df-uni 4832 df-int 4869 df-iun 4913 df-br 5059 df-opab 5121 df-mpt 5139 df-tr 5165 df-id 5454 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-res 5561 df-ima 5562 df-pred 6142 df-ord 6188 df-on 6189 df-lim 6190 df-suc 6191 df-iota 6308 df-fun 6351 df-fn 6352 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 df-fv 6357 df-isom 6358 df-riota 7108 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-2o 8097 df-oadd 8100 df-er 8283 df-map 8402 df-en 8504 df-dom 8505 df-sdom 8506 df-fin 8507 df-sup 8900 df-dju 9324 df-card 9362 df-pnf 10671 df-mnf 10672 df-xr 10673 df-ltxr 10674 df-le 10675 df-sub 10866 df-neg 10867 df-nn 11633 df-n0 11892 df-xnn0 11962 df-z 11976 df-uz 12238 df-fz 12887 df-hash 13685

This theorem is referenced by: erdszelem9 32441

W3C validator