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

Theorem vdwlem12 15615
Description: Lemma for vdw 15617. 𝐾 = 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.
StepHypRef Expression
1 vdw.r . . . . . . 7 (𝜑𝑅 ∈ Fin)
2 hashcl 13084 . . . . . . 7 (𝑅 ∈ Fin → (#‘𝑅) ∈ ℕ0)
31, 2syl 17 . . . . . 6 (𝜑 → (#‘𝑅) ∈ ℕ0)
43nn0red 11297 . . . . 5 (𝜑 → (#‘𝑅) ∈ ℝ)
54ltp1d 10899 . . . 4 (𝜑 → (#‘𝑅) < ((#‘𝑅) + 1))
6 nn0p1nn 11277 . . . . . . 7 ((#‘𝑅) ∈ ℕ0 → ((#‘𝑅) + 1) ∈ ℕ)
73, 6syl 17 . . . . . 6 (𝜑 → ((#‘𝑅) + 1) ∈ ℕ)
87nnnn0d 11296 . . . . 5 (𝜑 → ((#‘𝑅) + 1) ∈ ℕ0)
9 hashfz1 13071 . . . . 5 (((#‘𝑅) + 1) ∈ ℕ0 → (#‘(1...((#‘𝑅) + 1))) = ((#‘𝑅) + 1))
108, 9syl 17 . . . 4 (𝜑 → (#‘(1...((#‘𝑅) + 1))) = ((#‘𝑅) + 1))
115, 10breqtrrd 4646 . . 3 (𝜑 → (#‘𝑅) < (#‘(1...((#‘𝑅) + 1))))
12 fzfi 12708 . . . 4 (1...((#‘𝑅) + 1)) ∈ Fin
13 hashsdom 13107 . . . 4 ((𝑅 ∈ Fin ∧ (1...((#‘𝑅) + 1)) ∈ Fin) → ((#‘𝑅) < (#‘(1...((#‘𝑅) + 1))) ↔ 𝑅 ≺ (1...((#‘𝑅) + 1))))
141, 12, 13sylancl 693 . . 3 (𝜑 → ((#‘𝑅) < (#‘(1...((#‘𝑅) + 1))) ↔ 𝑅 ≺ (1...((#‘𝑅) + 1))))
1511, 14mpbid 222 . 2 (𝜑𝑅 ≺ (1...((#‘𝑅) + 1)))
16 vdwlem12.f . . . . 5 (𝜑𝐹:(1...((#‘𝑅) + 1))⟶𝑅)
17 fveq2 6150 . . . . . . . . 9 (𝑧 = 𝑥 → (𝐹𝑧) = (𝐹𝑥))
18 fveq2 6150 . . . . . . . . 9 (𝑤 = 𝑦 → (𝐹𝑤) = (𝐹𝑦))
1917, 18eqeqan12d 2642 . . . . . . . 8 ((𝑧 = 𝑥𝑤 = 𝑦) → ((𝐹𝑧) = (𝐹𝑤) ↔ (𝐹𝑥) = (𝐹𝑦)))
20 eqeq12 2639 . . . . . . . 8 ((𝑧 = 𝑥𝑤 = 𝑦) → (𝑧 = 𝑤𝑥 = 𝑦))
2119, 20imbi12d 334 . . . . . . 7 ((𝑧 = 𝑥𝑤 = 𝑦) → (((𝐹𝑧) = (𝐹𝑤) → 𝑧 = 𝑤) ↔ ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
22 fveq2 6150 . . . . . . . . . 10 (𝑧 = 𝑦 → (𝐹𝑧) = (𝐹𝑦))
23 fveq2 6150 . . . . . . . . . 10 (𝑤 = 𝑥 → (𝐹𝑤) = (𝐹𝑥))
2422, 23eqeqan12d 2642 . . . . . . . . 9 ((𝑧 = 𝑦𝑤 = 𝑥) → ((𝐹𝑧) = (𝐹𝑤) ↔ (𝐹𝑦) = (𝐹𝑥)))
25 eqcom 2633 . . . . . . . . 9 ((𝐹𝑦) = (𝐹𝑥) ↔ (𝐹𝑥) = (𝐹𝑦))
2624, 25syl6bb 276 . . . . . . . 8 ((𝑧 = 𝑦𝑤 = 𝑥) → ((𝐹𝑧) = (𝐹𝑤) ↔ (𝐹𝑥) = (𝐹𝑦)))
27 eqeq12 2639 . . . . . . . . 9 ((𝑧 = 𝑦𝑤 = 𝑥) → (𝑧 = 𝑤𝑦 = 𝑥))
28 eqcom 2633 . . . . . . . . 9 (𝑦 = 𝑥𝑥 = 𝑦)
2927, 28syl6bb 276 . . . . . . . 8 ((𝑧 = 𝑦𝑤 = 𝑥) → (𝑧 = 𝑤𝑥 = 𝑦))
3026, 29imbi12d 334 . . . . . . 7 ((𝑧 = 𝑦𝑤 = 𝑥) → (((𝐹𝑧) = (𝐹𝑤) → 𝑧 = 𝑤) ↔ ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
31 elfznn 12309 . . . . . . . . . 10 (𝑥 ∈ (1...((#‘𝑅) + 1)) → 𝑥 ∈ ℕ)
3231nnred 10980 . . . . . . . . 9 (𝑥 ∈ (1...((#‘𝑅) + 1)) → 𝑥 ∈ ℝ)
3332ssriv 3592 . . . . . . . 8 (1...((#‘𝑅) + 1)) ⊆ ℝ
3433a1i 11 . . . . . . 7 (𝜑 → (1...((#‘𝑅) + 1)) ⊆ ℝ)
35 biidd 252 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) → (((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦) ↔ ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
36 simplr3 1103 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥𝑦)
37 vdwlem12.2 . . . . . . . . . . 11 (𝜑 → ¬ 2 MonoAP 𝐹)
3837ad2antrr 761 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ¬ 2 MonoAP 𝐹)
39 3simpa 1056 . . . . . . . . . . . 12 ((𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦) → (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1))))
40 simplrl 799 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ (1...((#‘𝑅) + 1)))
4140, 31syl 17 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℕ)
42 simprr 795 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 < 𝑦)
43 simplrr 800 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ (1...((#‘𝑅) + 1)))
44 elfznn 12309 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ (1...((#‘𝑅) + 1)) → 𝑦 ∈ ℕ)
4543, 44syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℕ)
46 nnsub 11004 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (𝑥 < 𝑦 ↔ (𝑦𝑥) ∈ ℕ))
4741, 45, 46syl2anc 692 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 < 𝑦 ↔ (𝑦𝑥) ∈ ℕ))
4842, 47mpbid 222 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝑦𝑥) ∈ ℕ)
49 df-2 11024 . . . . . . . . . . . . . . . . . . 19 2 = (1 + 1)
5049fveq2i 6153 . . . . . . . . . . . . . . . . . 18 (AP‘2) = (AP‘(1 + 1))
5150oveqi 6618 . . . . . . . . . . . . . . . . 17 (𝑥(AP‘2)(𝑦𝑥)) = (𝑥(AP‘(1 + 1))(𝑦𝑥))
52 1nn0 11253 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℕ0
5352a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 1 ∈ ℕ0)
54 vdwapun 15597 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℕ0𝑥 ∈ ℕ ∧ (𝑦𝑥) ∈ ℕ) → (𝑥(AP‘(1 + 1))(𝑦𝑥)) = ({𝑥} ∪ ((𝑥 + (𝑦𝑥))(AP‘1)(𝑦𝑥))))
5553, 41, 48, 54syl3anc 1323 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝑥(AP‘(1 + 1))(𝑦𝑥)) = ({𝑥} ∪ ((𝑥 + (𝑦𝑥))(AP‘1)(𝑦𝑥))))
5651, 55syl5eq 2672 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝑥(AP‘2)(𝑦𝑥)) = ({𝑥} ∪ ((𝑥 + (𝑦𝑥))(AP‘1)(𝑦𝑥))))
57 simprl 793 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝐹𝑥) = (𝐹𝑦))
5816ad2antrr 761 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝐹:(1...((#‘𝑅) + 1))⟶𝑅)
59 ffn 6004 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:(1...((#‘𝑅) + 1))⟶𝑅𝐹 Fn (1...((#‘𝑅) + 1)))
6058, 59syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝐹 Fn (1...((#‘𝑅) + 1)))
61 fniniseg 6295 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Fn (1...((#‘𝑅) + 1)) → (𝑥 ∈ (𝐹 “ {(𝐹𝑦)}) ↔ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹𝑥) = (𝐹𝑦))))
6260, 61syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 ∈ (𝐹 “ {(𝐹𝑦)}) ↔ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹𝑥) = (𝐹𝑦))))
6340, 57, 62mpbir2and 956 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ (𝐹 “ {(𝐹𝑦)}))
6463snssd 4314 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → {𝑥} ⊆ (𝐹 “ {(𝐹𝑦)}))
6541nncnd 10981 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝑥 ∈ ℂ)
6645nncnd 10981 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ ℂ)
6765, 66pncan3d 10340 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝑥 + (𝑦𝑥)) = 𝑦)
6867oveq1d 6620 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → ((𝑥 + (𝑦𝑥))(AP‘1)(𝑦𝑥)) = (𝑦(AP‘1)(𝑦𝑥)))
69 vdwap1 15600 . . . . . . . . . . . . . . . . . . . 20 ((𝑦 ∈ ℕ ∧ (𝑦𝑥) ∈ ℕ) → (𝑦(AP‘1)(𝑦𝑥)) = {𝑦})
7045, 48, 69syl2anc 692 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝑦(AP‘1)(𝑦𝑥)) = {𝑦})
7168, 70eqtrd 2660 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → ((𝑥 + (𝑦𝑥))(AP‘1)(𝑦𝑥)) = {𝑦})
72 eqidd 2627 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝐹𝑦) = (𝐹𝑦))
73 fniniseg 6295 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn (1...((#‘𝑅) + 1)) → (𝑦 ∈ (𝐹 “ {(𝐹𝑦)}) ↔ (𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹𝑦) = (𝐹𝑦))))
7460, 73syl 17 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝑦 ∈ (𝐹 “ {(𝐹𝑦)}) ↔ (𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ (𝐹𝑦) = (𝐹𝑦))))
7543, 72, 74mpbir2and 956 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 𝑦 ∈ (𝐹 “ {(𝐹𝑦)}))
7675snssd 4314 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → {𝑦} ⊆ (𝐹 “ {(𝐹𝑦)}))
7771, 76eqsstrd 3623 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → ((𝑥 + (𝑦𝑥))(AP‘1)(𝑦𝑥)) ⊆ (𝐹 “ {(𝐹𝑦)}))
7864, 77unssd 3772 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → ({𝑥} ∪ ((𝑥 + (𝑦𝑥))(AP‘1)(𝑦𝑥))) ⊆ (𝐹 “ {(𝐹𝑦)}))
7956, 78eqsstrd 3623 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (𝑥(AP‘2)(𝑦𝑥)) ⊆ (𝐹 “ {(𝐹𝑦)}))
80 oveq1 6612 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑥 → (𝑎(AP‘2)𝑑) = (𝑥(AP‘2)𝑑))
8180sseq1d 3616 . . . . . . . . . . . . . . . 16 (𝑎 = 𝑥 → ((𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {(𝐹𝑦)}) ↔ (𝑥(AP‘2)𝑑) ⊆ (𝐹 “ {(𝐹𝑦)})))
82 oveq2 6613 . . . . . . . . . . . . . . . . 17 (𝑑 = (𝑦𝑥) → (𝑥(AP‘2)𝑑) = (𝑥(AP‘2)(𝑦𝑥)))
8382sseq1d 3616 . . . . . . . . . . . . . . . 16 (𝑑 = (𝑦𝑥) → ((𝑥(AP‘2)𝑑) ⊆ (𝐹 “ {(𝐹𝑦)}) ↔ (𝑥(AP‘2)(𝑦𝑥)) ⊆ (𝐹 “ {(𝐹𝑦)})))
8481, 83rspc2ev 3313 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℕ ∧ (𝑦𝑥) ∈ ℕ ∧ (𝑥(AP‘2)(𝑦𝑥)) ⊆ (𝐹 “ {(𝐹𝑦)})) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {(𝐹𝑦)}))
8541, 48, 79, 84syl3anc 1323 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {(𝐹𝑦)}))
86 fvex 6160 . . . . . . . . . . . . . . 15 (𝐹𝑦) ∈ V
87 sneq 4163 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝐹𝑦) → {𝑐} = {(𝐹𝑦)})
8887imaeq2d 5429 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝐹𝑦) → (𝐹 “ {𝑐}) = (𝐹 “ {(𝐹𝑦)}))
8988sseq2d 3617 . . . . . . . . . . . . . . . 16 (𝑐 = (𝐹𝑦) → ((𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ (𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {(𝐹𝑦)})))
90892rexbidv 3055 . . . . . . . . . . . . . . 15 (𝑐 = (𝐹𝑦) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {(𝐹𝑦)})))
9186, 90spcev 3291 . . . . . . . . . . . . . 14 (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {(𝐹𝑦)}) → ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {𝑐}))
9285, 91syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {𝑐}))
93 ovex 6633 . . . . . . . . . . . . . 14 (1...((#‘𝑅) + 1)) ∈ V
94 2nn0 11254 . . . . . . . . . . . . . . 15 2 ∈ ℕ0
9594a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 2 ∈ ℕ0)
9693, 95, 58vdwmc 15601 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → (2 MonoAP 𝐹 ↔ ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘2)𝑑) ⊆ (𝐹 “ {𝑐})))
9792, 96mpbird 247 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 2 MonoAP 𝐹)
9839, 97sylanl2 682 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ ((𝐹𝑥) = (𝐹𝑦) ∧ 𝑥 < 𝑦)) → 2 MonoAP 𝐹)
9998expr 642 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥 < 𝑦 → 2 MonoAP 𝐹))
10038, 99mtod 189 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ (𝐹𝑥) = (𝐹𝑦)) → ¬ 𝑥 < 𝑦)
101 simplr1 1101 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ (1...((#‘𝑅) + 1)))
102101, 32syl 17 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 ∈ ℝ)
103 simplr2 1102 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ (1...((#‘𝑅) + 1)))
10433, 103sseldi 3586 . . . . . . . . . 10 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑦 ∈ ℝ)
105102, 104eqleltd 10126 . . . . . . . . 9 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥 = 𝑦 ↔ (𝑥𝑦 ∧ ¬ 𝑥 < 𝑦)))
10636, 100, 105mpbir2and 956 . . . . . . . 8 (((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
107106ex 450 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑥𝑦)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
10821, 30, 34, 35, 107wlogle 10506 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ (1...((#‘𝑅) + 1)) ∧ 𝑦 ∈ (1...((#‘𝑅) + 1)))) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
109108ralrimivva 2970 . . . . 5 (𝜑 → ∀𝑥 ∈ (1...((#‘𝑅) + 1))∀𝑦 ∈ (1...((#‘𝑅) + 1))((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
110 dff13 6467 . . . . 5 (𝐹:(1...((#‘𝑅) + 1))–1-1𝑅 ↔ (𝐹:(1...((#‘𝑅) + 1))⟶𝑅 ∧ ∀𝑥 ∈ (1...((#‘𝑅) + 1))∀𝑦 ∈ (1...((#‘𝑅) + 1))((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
11116, 109, 110sylanbrc 697 . . . 4 (𝜑𝐹:(1...((#‘𝑅) + 1))–1-1𝑅)
112 f1domg 7920 . . . 4 (𝑅 ∈ Fin → (𝐹:(1...((#‘𝑅) + 1))–1-1𝑅 → (1...((#‘𝑅) + 1)) ≼ 𝑅))
1131, 111, 112sylc 65 . . 3 (𝜑 → (1...((#‘𝑅) + 1)) ≼ 𝑅)
114 domnsym 8031 . . 3 ((1...((#‘𝑅) + 1)) ≼ 𝑅 → ¬ 𝑅 ≺ (1...((#‘𝑅) + 1)))
115113, 114syl 17 . 2 (𝜑 → ¬ 𝑅 ≺ (1...((#‘𝑅) + 1)))
11615, 115pm2.65i 185 1 ¬ 𝜑
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1992  wral 2912  wrex 2913  cun 3558  wss 3560  {csn 4153   class class class wbr 4618  ccnv 5078  cima 5082   Fn wfn 5845  wf 5846  1-1wf1 5847  cfv 5850  (class class class)co 6605  cdom 7898  csdm 7899  Fincfn 7900  cr 9880  1c1 9882   + caddc 9884   < clt 10019  cle 10020  cmin 10211  cn 10965  2c2 11015  0cn0 11237  ...cfz 12265  #chash 13054  APcvdwa 15588   MonoAP cvdwm 15589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5642  df-ord 5688  df-on 5689  df-lim 5690  df-suc 5691  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-om 7014  df-1st 7116  df-2nd 7117  df-wrecs 7353  df-recs 7414  df-rdg 7452  df-1o 7506  df-oadd 7510  df-er 7688  df-en 7901  df-dom 7902  df-sdom 7903  df-fin 7904  df-card 8710  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-nn 10966  df-2 11024  df-n0 11238  df-xnn0 11309  df-z 11323  df-uz 11632  df-fz 12266  df-hash 13055  df-vdwap 15591  df-vdwmc 15592
This theorem is referenced by:  vdwlem13  15616
  Copyright terms: Public domain W3C validator