vdwlem12 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > vdwlem12		Structured version Visualization version GIF version

Theorem vdwlem12 15696

Description: Lemma for vdw 15698. 𝐾 = 2 base case of induction. (Contributed by Mario Carneiro, 18-Aug-2014.)

**Hypotheses**
Ref	Expression
vdw.r	⊢ (𝜑 → 𝑅 ∈ Fin)
vdwlem12.f	⊢ (𝜑 → 𝐹:(1...((#‘𝑅) + 1))⟶𝑅)
vdwlem12.2	⊢ (𝜑 → ¬ 2 MonoAP 𝐹)

**Assertion**
Ref	Expression
vdwlem12	⊢ ¬ 𝜑

Proof of Theorem vdwlem12 Dummy variables 𝑎 𝑐 𝑑 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vdw.r	. . . . . . 7 ⊢ (𝜑 → 𝑅 ∈ Fin)
2		hashcl 13147	. . . . . . 7 ⊢ (𝑅 ∈ Fin → (#‘𝑅) ∈ ℕ₀)
3	1, 2	syl 17	. . . . . 6 ⊢ (𝜑 → (#‘𝑅) ∈ ℕ₀)
4	3	nn0red 11352	. . . . 5 ⊢ (𝜑 → (#‘𝑅) ∈ ℝ)
5	4	ltp1d 10954	. . . 4 ⊢ (𝜑 → (#‘𝑅) < ((#‘𝑅) + 1))
6		nn0p1nn 11332	. . . . . . 7 ⊢ ((#‘𝑅) ∈ ℕ₀ → ((#‘𝑅) + 1) ∈ ℕ)
7	3, 6	syl 17	. . . . . 6 ⊢ (𝜑 → ((#‘𝑅) + 1) ∈ ℕ)
8	7	nnnn0d 11351	. . . . 5 ⊢ (𝜑 → ((#‘𝑅) + 1) ∈ ℕ₀)
9		hashfz1 13134	. . . . 5 ⊢ (((#‘𝑅) + 1) ∈ ℕ₀ → (#‘(1...((#‘𝑅) + 1))) = ((#‘𝑅) + 1))
10	8, 9	syl 17	. . . 4 ⊢ (𝜑 → (#‘(1...((#‘𝑅) + 1))) = ((#‘𝑅) + 1))
11	5, 10	breqtrrd 4681	. . 3 ⊢ (𝜑 → (#‘𝑅) < (#‘(1...((#‘𝑅) + 1))))
12		fzfi 12771	. . . 4 ⊢ (1...((#‘𝑅) + 1)) ∈ Fin
13		hashsdom 13170	. . . 4 ⊢ ((𝑅 ∈ Fin ∧ (1...((#‘𝑅) + 1)) ∈ Fin) → ((#‘𝑅) < (#‘(1...((#‘𝑅) + 1))) ↔ 𝑅 ≺ (1...((#‘𝑅) + 1))))
14	1, 12, 13	sylancl 694	. . 3 ⊢ (𝜑 → ((#‘𝑅) < (#‘(1...((#‘𝑅) + 1))) ↔ 𝑅 ≺ (1...((#‘𝑅) + 1))))
15	11, 14	mpbid 222	. 2 ⊢ (𝜑 → 𝑅 ≺ (1...((#‘𝑅) + 1)))
16		vdwlem12.f	. . . . 5 ⊢ (𝜑 → 𝐹:(1...((#‘𝑅) + 1))⟶𝑅)
17		fveq2 6191	. . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥))
18		fveq2 6191	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → (𝐹‘𝑤) = (𝐹‘𝑦))
19	17, 18	eqeqan12d 2638	. . . . . . . 8 ⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
20		eqeq12 2635	. . . . . . . 8 ⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (𝑧 = 𝑤 ↔ 𝑥 = 𝑦))
21	19, 20	imbi12d 334	. . . . . . 7 ⊢ ((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → (((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
22		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦))
23		fveq2 6191	. . . . . . . . . 10 ⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥))
24	22, 23	eqeqan12d 2638	. . . . . . . . 9 ⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑦) = (𝐹‘𝑥)))
25		eqcom 2629	. . . . . . . . 9 ⊢ ((𝐹‘𝑦) = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = (𝐹‘𝑦))
26	24, 25	syl6bb 276	. . . . . . . 8 ⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑥) = (𝐹‘𝑦)))
27		eqeq12 2635	. . . . . . . . 9 ⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (𝑧 = 𝑤 ↔ 𝑦 = 𝑥))
28		eqcom 2629	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 ↔ 𝑥 = 𝑦)
29	27, 28	syl6bb 276	. . . . . . . 8 ⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (𝑧 = 𝑤 ↔ 𝑥 = 𝑦))
30	26, 29	imbi12d 334	. . . . . . 7 ⊢ ((𝑧 = 𝑦 ∧ 𝑤 = 𝑥) → (((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
31		elfznn 12370	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...((#‘𝑅) + 1)) → 𝑥 ∈ ℕ)
32	31	nnred 11035	. . . . . . . . 9 ⊢ (𝑥 ∈ (1...((#‘𝑅) + 1)) → 𝑥 ∈ ℝ)
33	32	ssriv 3607	. . . . . . . 8 ⊢ (1...((#‘𝑅) + 1)) ⊆ ℝ
34	33	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1...((#‘𝑅) + 1)) ⊆ ℝ)
35		biidd 252	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) → (((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦) ↔ ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
36		simplr3 1105	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 ≤ 𝑦)
37		vdwlem12.2	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ 2 MonoAP 𝐹)
38	37	ad2antrr 762	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ¬ 2 MonoAP 𝐹)
39		3simpa 1058	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦) → (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1))))
40		simplrl 800	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ (1...((#‘𝑅) + 1)))
41	40, 31	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℕ)
42		simprr 796	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 < 𝑦)
43		simplrr 801	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ (1...((#‘𝑅) + 1)))
44		elfznn 12370	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...((#‘𝑅) + 1)) → 𝑦 ∈ ℕ)
45	43, 44	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℕ)
46		nnsub 11059	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 < 𝑦 ↔ (𝑦 − 𝑥) ∈ ℕ))
47	41, 45, 46	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 < 𝑦 ↔ (𝑦 − 𝑥) ∈ ℕ))
48	42, 47	mpbid 222	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑦 − 𝑥) ∈ ℕ)
49		df-2 11079	. . . . . . . . . . . . . . . . . . 19 ⊢ 2 = (1 + 1)
50	49	fveq2i 6194	. . . . . . . . . . . . . . . . . 18 ⊢ (AP‘2) = (AP‘(1 + 1))
51	50	oveqi 6663	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥(AP‘2)(𝑦 − 𝑥)) = (𝑥(AP‘(1 + 1))(𝑦 − 𝑥))
52		1nn0 11308	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℕ₀
53	52	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 1 ∈ ℕ₀)
54		vdwapun 15678	. . . . . . . . . . . . . . . . . 18 ⊢ ((1 ∈ ℕ₀ ∧ 𝑥 ∈ ℕ ∧ (𝑦 − 𝑥) ∈ ℕ) → (𝑥(AP‘(1 + 1))(𝑦 − 𝑥)) = ({𝑥} ∪ ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥))))
55	53, 41, 48, 54	syl3anc 1326	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥(AP‘(1 + 1))(𝑦 − 𝑥)) = ({𝑥} ∪ ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥))))
56	51, 55	syl5eq 2668	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥(AP‘2)(𝑦 − 𝑥)) = ({𝑥} ∪ ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥))))
57		simprl 794	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑥) = (𝐹‘𝑦))
58	16	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝐹:(1...((#‘𝑅) + 1))⟶𝑅)
59		ffn 6045	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹:(1...((#‘𝑅) + 1))⟶𝑅 → 𝐹 Fn (1...((#‘𝑅) + 1)))
60	58, 59	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝐹 Fn (1...((#‘𝑅) + 1)))
61		fniniseg 6338	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Fn (1...((#‘𝑅) + 1)) → (𝑥 ∈ (^◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))))
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 ∈ (^◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))))
63	40, 57, 62	mpbir2and 957	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ (^◡𝐹 “ {(𝐹‘𝑦)}))
64	63	snssd 4340	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → {𝑥} ⊆ (^◡𝐹 “ {(𝐹‘𝑦)}))
65	41	nncnd 11036	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℂ)
66	45	nncnd 11036	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℂ)
67	65, 66	pncan3d 10395	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 + (𝑦 − 𝑥)) = 𝑦)
68	67	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥)) = (𝑦(AP‘1)(𝑦 − 𝑥)))
69		vdwap1 15681	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ ℕ ∧ (𝑦 − 𝑥) ∈ ℕ) → (𝑦(AP‘1)(𝑦 − 𝑥)) = {𝑦})
70	45, 48, 69	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑦(AP‘1)(𝑦 − 𝑥)) = {𝑦})
71	68, 70	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥)) = {𝑦})
72		eqidd 2623	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝐹‘𝑦) = (𝐹‘𝑦))
73		fniniseg 6338	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn (1...((#‘𝑅) + 1)) → (𝑦 ∈ (^◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹‘𝑦) = (𝐹‘𝑦))))
74	60, 73	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑦 ∈ (^◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹‘𝑦) = (𝐹‘𝑦))))
75	43, 72, 74	mpbir2and 957	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ (^◡𝐹 “ {(𝐹‘𝑦)}))
76	75	snssd 4340	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → {𝑦} ⊆ (^◡𝐹 “ {(𝐹‘𝑦)}))
77	71, 76	eqsstrd 3639	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥)) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)}))
78	64, 77	unssd 3789	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ({𝑥} ∪ ((𝑥 + (𝑦 − 𝑥))(AP‘1)(𝑦 − 𝑥))) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)}))
79	56, 78	eqsstrd 3639	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (𝑥(AP‘2)(𝑦 − 𝑥)) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)}))
80		oveq1 6657	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝑥 → (𝑎(AP‘2)𝑑) = (𝑥(AP‘2)𝑑))
81	80	sseq1d 3632	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = 𝑥 → ((𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑥(AP‘2)𝑑) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)})))
82		oveq2 6658	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = (𝑦 − 𝑥) → (𝑥(AP‘2)𝑑) = (𝑥(AP‘2)(𝑦 − 𝑥)))
83	82	sseq1d 3632	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = (𝑦 − 𝑥) → ((𝑥(AP‘2)𝑑) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)}) ↔ (𝑥(AP‘2)(𝑦 − 𝑥)) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)})))
84	81, 83	rspc2ev 3324	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ ℕ ∧ (𝑦 − 𝑥) ∈ ℕ ∧ (𝑥(AP‘2)(𝑦 − 𝑥)) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)})) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)}))
85	41, 48, 79, 84	syl3anc 1326	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)}))
86		fvex 6201	. . . . . . . . . . . . . . 15 ⊢ (𝐹‘𝑦) ∈ V
87		sneq 4187	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝐹‘𝑦) → {𝑐} = {(𝐹‘𝑦)})
88	87	imaeq2d 5466	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝐹‘𝑦) → (^◡𝐹 “ {𝑐}) = (^◡𝐹 “ {(𝐹‘𝑦)}))
89	88	sseq2d 3633	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = (𝐹‘𝑦) → ((𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {𝑐}) ↔ (𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)})))
90	89	2rexbidv 3057	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = (𝐹‘𝑦) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)})))
91	86, 90	spcev 3300	. . . . . . . . . . . . . 14 ⊢ (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {(𝐹‘𝑦)}) → ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {𝑐}))
92	85, 91	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {𝑐}))
93		ovex 6678	. . . . . . . . . . . . . 14 ⊢ (1...((#‘𝑅) + 1)) ∈ V
94		2nn0 11309	. . . . . . . . . . . . . . 15 ⊢ 2 ∈ ℕ₀
95	94	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈ ℕ₀)
96	93, 95, 58	vdwmc 15682	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → (2 MonoAP 𝐹 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (^◡𝐹 “ {𝑐})))
97	92, 96	mpbird 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 2 MonoAP 𝐹)
98	39, 97	sylanl2 683	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ ((𝐹‘𝑥) = (𝐹‘𝑦) ∧ 𝑥 < 𝑦)) → 2 MonoAP 𝐹)
99	98	expr 643	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝑥 < 𝑦 → 2 MonoAP 𝐹))
100	38, 99	mtod 189	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → ¬ 𝑥 < 𝑦)
101		simplr1 1103	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 ∈ (1...((#‘𝑅) + 1)))
102	101, 32	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 ∈ ℝ)
103		simplr2 1104	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑦 ∈ (1...((#‘𝑅) + 1)))
104	33, 103	sseldi 3601	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑦 ∈ ℝ)
105	102, 104	eqleltd 10181	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → (𝑥 = 𝑦 ↔ (𝑥 ≤ 𝑦 ∧ ¬ 𝑥 < 𝑦)))
106	36, 100, 105	mpbir2and 957	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) → 𝑥 = 𝑦)
107	106	ex 450	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥 ≤ 𝑦)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
108	21, 30, 34, 35, 107	wlogle 10561	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) → ((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
109	108	ralrimivva 2971	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ (1...((#‘𝑅) + 1))∀𝑦 ∈ (1...((#‘𝑅) + 1))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦))
110		dff13 6512	. . . . 5 ⊢ (𝐹:(1...((#‘𝑅) + 1))–1-1→𝑅 ↔ (𝐹:(1...((#‘𝑅) + 1))⟶𝑅 ∧ ∀𝑥 ∈ (1...((#‘𝑅) + 1))∀𝑦 ∈ (1...((#‘𝑅) + 1))((𝐹‘𝑥) = (𝐹‘𝑦) → 𝑥 = 𝑦)))
111	16, 109, 110	sylanbrc 698	. . . 4 ⊢ (𝜑 → 𝐹:(1...((#‘𝑅) + 1))–1-1→𝑅)
112		f1domg 7975	. . . 4 ⊢ (𝑅 ∈ Fin → (𝐹:(1...((#‘𝑅) + 1))–1-1→𝑅 → (1...((#‘𝑅) + 1)) ≼ 𝑅))
113	1, 111, 112	sylc 65	. . 3 ⊢ (𝜑 → (1...((#‘𝑅) + 1)) ≼ 𝑅)
114		domnsym 8086	. . 3 ⊢ ((1...((#‘𝑅) + 1)) ≼ 𝑅 → ¬ 𝑅 ≺ (1...((#‘𝑅) + 1)))
115	113, 114	syl 17	. 2 ⊢ (𝜑 → ¬ 𝑅 ≺ (1...((#‘𝑅) + 1)))
116	15, 115	pm2.65i 185	1 ⊢ ¬ 𝜑

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∃wex 1704 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 ∪ cun 3572 ⊆ wss 3574 {csn 4177 class class class wbr 4653 ^◡ccnv 5113 “ cima 5117 Fn wfn 5883 ⟶wf 5884 –1-1→wf1 5885 ‘cfv 5888 (class class class)co 6650 ≼ cdom 7953 ≺ csdm 7954 Fincfn 7955 ℝcr 9935 1c1 9937 + caddc 9939 < clt 10074 ≤ cle 10075 − cmin 10266 ℕcn 11020 2c2 11070 ℕ₀cn0 11292 ...cfz 12326 #chash 13117 APcvdwa 15669 MonoAP cvdwm 15670

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-hash 13118 df-vdwap 15672 df-vdwmc 15673

This theorem is referenced by: vdwlem13 15697

W3C validator