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 31458

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

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

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

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

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

Step	Hyp	Ref	Expression
1		hashf 13290	. . . . 5 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
2		ffun 6197	. . . . 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 31455	. . . . 5 ⊢ ((𝜑 ∧ 𝐴 ∈ (1...𝑁)) → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
10	4, 9	mpdan 705	. . . 4 ⊢ (𝜑 → (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}))
11		fvelima 6398	. . . 4 ⊢ ((Fun ♯ ∧ (𝐾‘𝐴) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)})) → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴))
12	3, 10, 11	sylancr 698	. . 3 ⊢ (𝜑 → ∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴))
13		eqid 2748	. . . . . 6 ⊢ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}
14	13	erdszelem1 31451	. . . . 5 ⊢ (𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} ↔ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓))
15		fzfid 12937	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ∈ Fin)
16		simplr1 1237	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝐴))
17		ssfi 8333	. . . . . . . . . . 11 ⊢ (((1...𝐴) ∈ Fin ∧ 𝑓 ⊆ (1...𝐴)) → 𝑓 ∈ Fin)
18	15, 16, 17	syl2anc 696	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ∈ Fin)
19		hashcl 13310	. . . . . . . . . 10 ⊢ (𝑓 ∈ Fin → (♯‘𝑓) ∈ ℕ₀)
20	18, 19	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ∈ ℕ₀)
21	20	nn0red 11515	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ∈ ℝ)
22		eqid 2748	. . . . . . . . . . . . . . 15 ⊢ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} = {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}
23	22	erdszelem2 31452	. . . . . . . . . . . . . 14 ⊢ ((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℕ)
24	23	simpri 481	. . . . . . . . . . . . 13 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℕ
25		nnssre 11187	. . . . . . . . . . . . 13 ⊢ ℕ ⊆ ℝ
26	24, 25	sstri 3741	. . . . . . . . . . . 12 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ
27	26	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ)
28		erdszelem.l	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐴 < 𝐵)
29		elfznn 12534	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℕ)
30	4, 29	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℕ)
31	30	nnred 11198	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐴 ∈ ℝ)
32		erdszelem.b	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐵 ∈ (1...𝑁))
33		elfznn 12534	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℕ)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℕ)
35	34	nnred 11198	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ ℝ)
36	31, 35	ltnled 10347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
37	28, 36	mpbid 222	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ¬ 𝐵 ≤ 𝐴)
38		elfzle2 12509	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ (1...𝐴) → 𝐵 ≤ 𝐴)
39	37, 38	nsyl 135	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝐵 ∈ (1...𝐴))
40	39	ad2antrr 764	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ¬ 𝐵 ∈ (1...𝐴))
41	16, 40	ssneldd 3735	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ¬ 𝐵 ∈ 𝑓)
42	32	ad2antrr 764	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (1...𝑁))
43		hashunsng 13344	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ (1...𝑁) → ((𝑓 ∈ Fin ∧ ¬ 𝐵 ∈ 𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
44	42, 43	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝑓 ∈ Fin ∧ ¬ 𝐵 ∈ 𝑓) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1)))
45	18, 41, 44	mp2and 717	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘(𝑓 ∪ {𝐵})) = ((♯‘𝑓) + 1))
46		elfzelz 12506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ (1...𝑁) → 𝐴 ∈ ℤ)
47	4, 46	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ∈ ℤ)
48		elfzelz 12506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐵 ∈ (1...𝑁) → 𝐵 ∈ ℤ)
49	32, 48	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐵 ∈ ℤ)
50	31, 35, 28	ltled 10348	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
51		eluz2 11856	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) ↔ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≤ 𝐵))
52	47, 49, 50, 51	syl3anbrc 1407	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐵 ∈ (ℤ_≥‘𝐴))
53		fzss2 12545	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ (ℤ_≥‘𝐴) → (1...𝐴) ⊆ (1...𝐵))
54	52, 53	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1...𝐴) ⊆ (1...𝐵))
55	54	ad2antrr 764	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ⊆ (1...𝐵))
56	16, 55	sstrd 3742	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝐵))
57		elfz1end 12535	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ ℕ ↔ 𝐵 ∈ (1...𝐵))
58	34, 57	sylib 208	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ (1...𝐵))
59	58	ad2antrr 764	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (1...𝐵))
60	59	snssd 4473	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → {𝐵} ⊆ (1...𝐵))
61	56, 60	unssd 3920	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝐵))
62		simplr2 1239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)))
63		f1f 6250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝐹:(1...𝑁)–1-1→ℝ → 𝐹:(1...𝑁)⟶ℝ)
64	6, 63	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝐹:(1...𝑁)⟶ℝ)
65	64	ad2antrr 764	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐹:(1...𝑁)⟶ℝ)
66		elfzuz3 12503	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∈ (1...𝑁) → 𝑁 ∈ (ℤ_≥‘𝐴))
67		fzss2 12545	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ (ℤ_≥‘𝐴) → (1...𝐴) ⊆ (1...𝑁))
68	4, 66, 67	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → (1...𝐴) ⊆ (1...𝑁))
69	68	ad2antrr 764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (1...𝐴) ⊆ (1...𝑁))
70	16, 69	sstrd 3742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝑓 ⊆ (1...𝑁))
71		fzssuz 12546	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (1...𝑁) ⊆ (ℤ_≥‘1)
72		uzssz 11870	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℤ_≥‘1) ⊆ ℤ
73		zssre 11547	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ℤ ⊆ ℝ
74	72, 73	sstri 3741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℤ_≥‘1) ⊆ ℝ
75	71, 74	sstri 3741	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1...𝑁) ⊆ ℝ
76		ltso 10281	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ < Or ℝ
77		soss 5193	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((1...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (1...𝑁)))
78	75, 76, 77	mp2 9	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ < Or (1...𝑁)
79		soisores 6728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁))) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
80	78, 8, 79	mpanl12 720	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐹:(1...𝑁)⟶ℝ ∧ 𝑓 ⊆ (1...𝑁)) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
81	65, 70, 80	syl2anc 696	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ↔ ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
82	62, 81	mpbid 222	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
83	82	r19.21bi 3058	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
84	16	sselda 3732	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ (1...𝐴))
85		elfzle2 12509	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑧 ∈ (1...𝐴) → 𝑧 ≤ 𝐴)
86	84, 85	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ≤ 𝐴)
87	70	sselda 3732	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ (1...𝑁))
88	75, 87	sseldi 3730	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ ℝ)
89	4	ad3antrrr 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ (1...𝑁))
90	89, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ ℕ)
91	90	nnred 11198	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ ℝ)
92	88, 91	lenltd 10346	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑧 ≤ 𝐴 ↔ ¬ 𝐴 < 𝑧))
93	86, 92	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ¬ 𝐴 < 𝑧)
94	62	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)))
95		simplr3 1241	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐴 ∈ 𝑓)
96	95	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐴 ∈ 𝑓)
97		simpr 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝑧 ∈ 𝑓)
98		isorel 6727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (𝐴 < 𝑧 ↔ ((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧)))
99		fvres 6356	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝐴 ∈ 𝑓 → ((𝐹 ↾ 𝑓)‘𝐴) = (𝐹‘𝐴))
100		fvres 6356	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑧 ∈ 𝑓 → ((𝐹 ↾ 𝑓)‘𝑧) = (𝐹‘𝑧))
101	99, 100	breqan12d 4808	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓) → (((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧) ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
102	101	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (((𝐹 ↾ 𝑓)‘𝐴)𝑂((𝐹 ↾ 𝑓)‘𝑧) ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
103	98, 102	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ (𝐴 ∈ 𝑓 ∧ 𝑧 ∈ 𝑓)) → (𝐴 < 𝑧 ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
104	94, 96, 97, 103	syl12anc 1461	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐴 < 𝑧 ↔ (𝐹‘𝐴)𝑂(𝐹‘𝑧)))
105	93, 104	mtbid 313	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧))
106		simplr 809	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐴)𝑂(𝐹‘𝐵))
107	65	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐹:(1...𝑁)⟶ℝ)
108	107, 87	ffvelrnd 6511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝑧) ∈ ℝ)
109	107, 89	ffvelrnd 6511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐴) ∈ ℝ)
110	42	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → 𝐵 ∈ (1...𝑁))
111	107, 110	ffvelrnd 6511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝐵) ∈ ℝ)
112		sotr2 5204	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑂 Or ℝ ∧ ((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ)) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
113	8, 112	mpan 708	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝐹‘𝑧) ∈ ℝ ∧ (𝐹‘𝐴) ∈ ℝ ∧ (𝐹‘𝐵) ∈ ℝ) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
114	108, 109, 111, 113	syl3anc 1463	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ((¬ (𝐹‘𝐴)𝑂(𝐹‘𝑧) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
115	105, 106, 114	mp2and 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝐹‘𝑧)𝑂(𝐹‘𝐵))
116	115	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
117		elsni 4326	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ {𝐵} → 𝑤 = 𝐵)
118	117	fveq2d 6344	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ {𝐵} → (𝐹‘𝑤) = (𝐹‘𝐵))
119	118	breq2d 4804	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ {𝐵} → ((𝐹‘𝑧)𝑂(𝐹‘𝑤) ↔ (𝐹‘𝑧)𝑂(𝐹‘𝐵)))
120	119	imbi2d 329	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝐵))))
121	116, 120	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → (𝑤 ∈ {𝐵} → (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
122	121	ralrimiv 3091	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
123		ralunb 3925	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (∀𝑤 ∈ 𝑓 (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ∧ ∀𝑤 ∈ {𝐵} (𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
124	83, 122, 123	sylanbrc 701	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑧 ∈ 𝑓) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
125	124	ralrimiva 3092	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ 𝑓 ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
126	61	sselda 3732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → 𝑤 ∈ (1...𝐵))
127		elfzle2 12509	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ≤ 𝐵)
128	127	adantl 473	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ≤ 𝐵)
129		elfzelz 12506	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℤ)
130	129	zred 11645	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 ∈ (1...𝐵) → 𝑤 ∈ ℝ)
131	130	adantl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝑤 ∈ ℝ)
132	35	ad3antrrr 768	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → 𝐵 ∈ ℝ)
133	131, 132	lenltd 10346	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → (𝑤 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑤))
134	128, 133	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (1...𝐵)) → ¬ 𝐵 < 𝑤)
135	126, 134	syldan 488	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → ¬ 𝐵 < 𝑤)
136	135	pm2.21d 118	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) ∧ 𝑤 ∈ (𝑓 ∪ {𝐵})) → (𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
137	136	ralrimiva 3092	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
138		elsni 4326	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 ∈ {𝐵} → 𝑧 = 𝐵)
139	138	breq1d 4802	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 ∈ {𝐵} → (𝑧 < 𝑤 ↔ 𝐵 < 𝑤))
140	139	imbi1d 330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 ∈ {𝐵} → ((𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
141	140	ralbidv 3112	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ {𝐵} → (∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝐵 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
142	137, 141	syl5ibrcom 237	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑧 ∈ {𝐵} → ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
143	142	ralrimiv 3091	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
144		ralunb 3925	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ↔ (∀𝑧 ∈ 𝑓 ∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)) ∧ ∀𝑧 ∈ {𝐵}∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
145	125, 143, 144	sylanbrc 701	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤)))
146	42	snssd 4473	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → {𝐵} ⊆ (1...𝑁))
147	70, 146	unssd 3920	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))
148		soisores 6728	. . . . . . . . . . . . . . . . . 18 ⊢ ((( < Or (1...𝑁) ∧ 𝑂 Or ℝ) ∧ (𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁))) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
149	78, 8, 148	mpanl12 720	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:(1...𝑁)⟶ℝ ∧ (𝑓 ∪ {𝐵}) ⊆ (1...𝑁)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
150	65, 147, 149	syl2anc 696	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ↔ ∀𝑧 ∈ (𝑓 ∪ {𝐵})∀𝑤 ∈ (𝑓 ∪ {𝐵})(𝑧 < 𝑤 → (𝐹‘𝑧)𝑂(𝐹‘𝑤))))
151	145, 150	mpbird 247	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))))
152		ssun2 3908	. . . . . . . . . . . . . . . 16 ⊢ {𝐵} ⊆ (𝑓 ∪ {𝐵})
153		snssg 4447	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ (1...𝐵) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
154	59, 153	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐵 ∈ (𝑓 ∪ {𝐵}) ↔ {𝐵} ⊆ (𝑓 ∪ {𝐵})))
155	152, 154	mpbiri 248	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → 𝐵 ∈ (𝑓 ∪ {𝐵}))
156	22	erdszelem1 31451	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} ↔ ((𝑓 ∪ {𝐵}) ⊆ (1...𝐵) ∧ (𝐹 ↾ (𝑓 ∪ {𝐵})) Isom < , 𝑂 ((𝑓 ∪ {𝐵}), (𝐹 “ (𝑓 ∪ {𝐵}))) ∧ 𝐵 ∈ (𝑓 ∪ {𝐵})))
157	61, 151, 155, 156	syl3anbrc 1407	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})
158		vex 3331	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
159		snex 5045	. . . . . . . . . . . . . . . . 17 ⊢ {𝐵} ∈ V
160	158, 159	unex 7109	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∪ {𝐵}) ∈ V
161	1	fdmi 6201	. . . . . . . . . . . . . . . 16 ⊢ dom ♯ = V
162	160, 161	eleqtrri 2826	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∪ {𝐵}) ∈ dom ♯
163		funfvima 6643	. . . . . . . . . . . . . . 15 ⊢ ((Fun ♯ ∧ (𝑓 ∪ {𝐵}) ∈ dom ♯) → ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})))
164	3, 162, 163	mp2an 710	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∪ {𝐵}) ∈ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)} → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
165	157, 164	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘(𝑓 ∪ {𝐵})) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
166	45, 165	eqeltrrd 2828	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}))
167		ne0i 4052	. . . . . . . . . . . 12 ⊢ (((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ≠ ∅)
168	166, 167	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ≠ ∅)
169	23	simpli 476	. . . . . . . . . . . 12 ⊢ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin
170		fimaxre2 11132	. . . . . . . . . . . 12 ⊢ (((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧)
171	27, 169, 170	sylancl 697	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧)
172		suprub 11147	. . . . . . . . . . 11 ⊢ ((((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ⊆ ℝ ∧ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}) ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})𝑤 ≤ 𝑧) ∧ ((♯‘𝑓) + 1) ∈ (♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)})) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
173	27, 168, 171, 166, 172	syl31anc 1466	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ≤ sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
174	5, 6, 7	erdszelem3 31453	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ (1...𝑁) → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
175	32, 174	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
176	175	ad2antrr 764	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) = sup((♯ “ {𝑦 ∈ 𝒫 (1...𝐵) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐵 ∈ 𝑦)}), ℝ, < ))
177	173, 176	breqtrrd 4820	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵))
178	5, 6, 7, 8	erdszelem6 31456	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾:(1...𝑁)⟶ℕ)
179	178, 32	ffvelrnd 6511	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾‘𝐵) ∈ ℕ)
180	179	ad2antrr 764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) ∈ ℕ)
181	180	nnnn0d 11514	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (𝐾‘𝐵) ∈ ℕ₀)
182		nn0ltp1le 11598	. . . . . . . . . 10 ⊢ (((♯‘𝑓) ∈ ℕ₀ ∧ (𝐾‘𝐵) ∈ ℕ₀) → ((♯‘𝑓) < (𝐾‘𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵)))
183	20, 181, 182	syl2anc 696	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → ((♯‘𝑓) < (𝐾‘𝐵) ↔ ((♯‘𝑓) + 1) ≤ (𝐾‘𝐵)))
184	177, 183	mpbird 247	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) < (𝐾‘𝐵))
185	21, 184	ltned 10336	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) ∧ (𝐹‘𝐴)𝑂(𝐹‘𝐵)) → (♯‘𝑓) ≠ (𝐾‘𝐵))
186	185	ex 449	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (♯‘𝑓) ≠ (𝐾‘𝐵)))
187		neeq1 2982	. . . . . . 7 ⊢ ((♯‘𝑓) = (𝐾‘𝐴) → ((♯‘𝑓) ≠ (𝐾‘𝐵) ↔ (𝐾‘𝐴) ≠ (𝐾‘𝐵)))
188	187	imbi2d 329	. . . . . 6 ⊢ ((♯‘𝑓) = (𝐾‘𝐴) → (((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (♯‘𝑓) ≠ (𝐾‘𝐵)) ↔ ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
189	186, 188	syl5ibcom 235	. . . . 5 ⊢ ((𝜑 ∧ (𝑓 ⊆ (1...𝐴) ∧ (𝐹 ↾ 𝑓) Isom < , 𝑂 (𝑓, (𝐹 “ 𝑓)) ∧ 𝐴 ∈ 𝑓)) → ((♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
190	14, 189	sylan2b 493	. . . 4 ⊢ ((𝜑 ∧ 𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)}) → ((♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
191	190	rexlimdva 3157	. . 3 ⊢ (𝜑 → (∃𝑓 ∈ {𝑦 ∈ 𝒫 (1...𝐴) ∣ ((𝐹 ↾ 𝑦) Isom < , 𝑂 (𝑦, (𝐹 “ 𝑦)) ∧ 𝐴 ∈ 𝑦)} (♯‘𝑓) = (𝐾‘𝐴) → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵))))
192	12, 191	mpd 15	. 2 ⊢ (𝜑 → ((𝐹‘𝐴)𝑂(𝐹‘𝐵) → (𝐾‘𝐴) ≠ (𝐾‘𝐵)))
193	192	necon2bd 2936	1 ⊢ (𝜑 → ((𝐾‘𝐴) = (𝐾‘𝐵) → ¬ (𝐹‘𝐴)𝑂(𝐹‘𝐵)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 383 ∧ w3a 1072 = wceq 1620 ∈ wcel 2127 ≠ wne 2920 ∀wral 3038 ∃wrex 3039 {crab 3042 Vcvv 3328 ∪ cun 3701 ⊆ wss 3703 ∅c0 4046 𝒫 cpw 4290 {csn 4309 class class class wbr 4792 ↦ cmpt 4869 Or wor 5174 dom cdm 5254 ↾ cres 5256 “ cima 5257 Fun wfun 6031 ⟶wf 6033 –1-1→wf1 6034 ‘cfv 6037 Isom wiso 6038 (class class class)co 6801 Fincfn 8109 supcsup 8499 ℝcr 10098 1c1 10100 + caddc 10102 +∞cpnf 10234 < clt 10237 ≤ cle 10238 ℕcn 11183 ℕ₀cn0 11455 ℤcz 11540 ℤ_≥cuz 11850 ...cfz 12490 ♯chash 13282

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-rep 4911 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-cnex 10155 ax-resscn 10156 ax-1cn 10157 ax-icn 10158 ax-addcl 10159 ax-addrcl 10160 ax-mulcl 10161 ax-mulrcl 10162 ax-mulcom 10163 ax-addass 10164 ax-mulass 10165 ax-distr 10166 ax-i2m1 10167 ax-1ne0 10168 ax-1rid 10169 ax-rnegex 10170 ax-rrecex 10171 ax-cnre 10172 ax-pre-lttri 10173 ax-pre-lttrn 10174 ax-pre-ltadd 10175 ax-pre-mulgt0 10176 ax-pre-sup 10177

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-nel 3024 df-ral 3043 df-rex 3044 df-reu 3045 df-rmo 3046 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-pss 3719 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-tp 4314 df-op 4316 df-uni 4577 df-int 4616 df-iun 4662 df-br 4793 df-opab 4853 df-mpt 4870 df-tr 4893 df-id 5162 df-eprel 5167 df-po 5175 df-so 5176 df-fr 5213 df-we 5215 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-pred 5829 df-ord 5875 df-on 5876 df-lim 5877 df-suc 5878 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-isom 6046 df-riota 6762 df-ov 6804 df-oprab 6805 df-mpt2 6806 df-om 7219 df-1st 7321 df-2nd 7322 df-wrecs 7564 df-recs 7625 df-rdg 7663 df-1o 7717 df-2o 7718 df-oadd 7721 df-er 7899 df-map 8013 df-en 8110 df-dom 8111 df-sdom 8112 df-fin 8113 df-sup 8501 df-card 8926 df-cda 9153 df-pnf 10239 df-mnf 10240 df-xr 10241 df-ltxr 10242 df-le 10243 df-sub 10431 df-neg 10432 df-nn 11184 df-n0 11456 df-xnn0 11527 df-z 11541 df-uz 11851 df-fz 12491 df-hash 13283

This theorem is referenced by: erdszelem9 31459

W3C validator