Step | Hyp | Ref
| Expression |
1 | | vdwlem1.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℕ) |
2 | | vdwlem1.d |
. . . . 5
⊢ (𝜑 → 𝐷:(1...𝑀)⟶ℕ) |
3 | | vdwlem1.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (1...𝑀)) |
4 | 2, 3 | ffvelrnd 6360 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐼) ∈ ℕ) |
5 | | vdwlem1.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℕ) |
6 | 5 | nnnn0d 11351 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
7 | | vdwapun 15678 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝐴 ∈ ℕ
∧ (𝐷‘𝐼) ∈ ℕ) → (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼)) = ({𝐴} ∪ ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)))) |
8 | 6, 1, 4, 7 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼)) = ({𝐴} ∪ ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)))) |
9 | 1 | nnred 11035 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
10 | | vdwlem1.m |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℕ) |
11 | | nnuz 11723 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
12 | 10, 11 | syl6eleq 2711 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
13 | | eluzfz1 12348 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑀)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈ (1...𝑀)) |
15 | 2, 14 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘1) ∈ ℕ) |
16 | 1, 15 | nnaddcld 11067 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + (𝐷‘1)) ∈ ℕ) |
17 | 16 | nnred 11035 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + (𝐷‘1)) ∈ ℝ) |
18 | | vdwlem1.w |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ ℕ) |
19 | 18 | nnred 11035 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ ℝ) |
20 | 15 | nnrpd 11870 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘1) ∈
ℝ+) |
21 | 9, 20 | ltaddrpd 11905 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < (𝐴 + (𝐷‘1))) |
22 | 9, 17, 21 | ltled 10185 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≤ (𝐴 + (𝐷‘1))) |
23 | | vdwlem1.s |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))})) |
24 | 23 | r19.21bi 2932 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))})) |
25 | | cnvimass 5485 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) ⊆ dom 𝐹 |
26 | | vdwlem1.f |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹:(1...𝑊)⟶𝑅) |
27 | | fdm 6051 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:(1...𝑊)⟶𝑅 → dom 𝐹 = (1...𝑊)) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → dom 𝐹 = (1...𝑊)) |
29 | 25, 28 | syl5sseq 3653 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) ⊆ (1...𝑊)) |
30 | 29 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) ⊆ (1...𝑊)) |
31 | 24, 30 | sstrd 3613 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (1...𝑊)) |
32 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
33 | 5, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐾 − 1) ∈
ℕ0) |
34 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) |
35 | 33, 34 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐾 − 1) ∈
(ℤ≥‘0)) |
36 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 − 1) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝐾 − 1))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ∈ (0...(𝐾 − 1))) |
38 | 37 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 0 ∈ (0...(𝐾 − 1))) |
39 | 2 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐷‘𝑖) ∈ ℕ) |
40 | 39 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐷‘𝑖) ∈ ℂ) |
41 | 40 | mul02d 10234 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (0 · (𝐷‘𝑖)) = 0) |
42 | 41 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐴 + (𝐷‘𝑖)) + (0 · (𝐷‘𝑖))) = ((𝐴 + (𝐷‘𝑖)) + 0)) |
43 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐴 ∈ ℕ) |
44 | 43, 39 | nnaddcld 11067 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐴 + (𝐷‘𝑖)) ∈ ℕ) |
45 | 44 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐴 + (𝐷‘𝑖)) ∈ ℂ) |
46 | 45 | addid1d 10236 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐴 + (𝐷‘𝑖)) + 0) = (𝐴 + (𝐷‘𝑖))) |
47 | 42, 46 | eqtr2d 2657 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (0 · (𝐷‘𝑖)))) |
48 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 0 → (𝑚 · (𝐷‘𝑖)) = (0 · (𝐷‘𝑖))) |
49 | 48 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = 0 → ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖))) = ((𝐴 + (𝐷‘𝑖)) + (0 · (𝐷‘𝑖)))) |
50 | 49 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 0 → ((𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖))) ↔ (𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (0 · (𝐷‘𝑖))))) |
51 | 50 | rspcev 3309 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ (0...(𝐾 − 1))
∧ (𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (0 · (𝐷‘𝑖)))) → ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖)))) |
52 | 38, 47, 51 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖)))) |
53 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ) |
54 | 53 | nnnn0d 11351 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈
ℕ0) |
55 | | vdwapval 15677 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℕ0
∧ (𝐴 + (𝐷‘𝑖)) ∈ ℕ ∧ (𝐷‘𝑖) ∈ ℕ) → ((𝐴 + (𝐷‘𝑖)) ∈ ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖))))) |
56 | 54, 44, 39, 55 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐴 + (𝐷‘𝑖)) ∈ ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖))))) |
57 | 52, 56 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐴 + (𝐷‘𝑖)) ∈ ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖))) |
58 | 31, 57 | sseldd 3604 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐴 + (𝐷‘𝑖)) ∈ (1...𝑊)) |
59 | 58 | ralrimiva 2966 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)(𝐴 + (𝐷‘𝑖)) ∈ (1...𝑊)) |
60 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = 1 → (𝐷‘𝑖) = (𝐷‘1)) |
61 | 60 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → (𝐴 + (𝐷‘𝑖)) = (𝐴 + (𝐷‘1))) |
62 | 61 | eleq1d 2686 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → ((𝐴 + (𝐷‘𝑖)) ∈ (1...𝑊) ↔ (𝐴 + (𝐷‘1)) ∈ (1...𝑊))) |
63 | 62 | rspcv 3305 |
. . . . . . . . . . . 12
⊢ (1 ∈
(1...𝑀) →
(∀𝑖 ∈
(1...𝑀)(𝐴 + (𝐷‘𝑖)) ∈ (1...𝑊) → (𝐴 + (𝐷‘1)) ∈ (1...𝑊))) |
64 | 14, 59, 63 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + (𝐷‘1)) ∈ (1...𝑊)) |
65 | | elfzle2 12345 |
. . . . . . . . . . 11
⊢ ((𝐴 + (𝐷‘1)) ∈ (1...𝑊) → (𝐴 + (𝐷‘1)) ≤ 𝑊) |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + (𝐷‘1)) ≤ 𝑊) |
67 | 9, 17, 19, 22, 66 | letrd 10194 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝑊) |
68 | 1, 11 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘1)) |
69 | 18 | nnzd 11481 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ ℤ) |
70 | | elfz5 12334 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘1) ∧ 𝑊 ∈ ℤ) → (𝐴 ∈ (1...𝑊) ↔ 𝐴 ≤ 𝑊)) |
71 | 68, 69, 70 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ (1...𝑊) ↔ 𝐴 ≤ 𝑊)) |
72 | 67, 71 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ (1...𝑊)) |
73 | | eqidd 2623 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐴)) |
74 | | ffn 6045 |
. . . . . . . . 9
⊢ (𝐹:(1...𝑊)⟶𝑅 → 𝐹 Fn (1...𝑊)) |
75 | | fniniseg 6338 |
. . . . . . . . 9
⊢ (𝐹 Fn (1...𝑊) → (𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ (𝐴 ∈ (1...𝑊) ∧ (𝐹‘𝐴) = (𝐹‘𝐴)))) |
76 | 26, 74, 75 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ (𝐴 ∈ (1...𝑊) ∧ (𝐹‘𝐴) = (𝐹‘𝐴)))) |
77 | 72, 73, 76 | mpbir2and 957 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)})) |
78 | 77 | snssd 4340 |
. . . . . 6
⊢ (𝜑 → {𝐴} ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
79 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (𝐷‘𝑖) = (𝐷‘𝐼)) |
80 | 79 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → (𝐴 + (𝐷‘𝑖)) = (𝐴 + (𝐷‘𝐼))) |
81 | 80, 79 | oveq12d 6668 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼))) |
82 | 80 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝐼 → (𝐹‘(𝐴 + (𝐷‘𝑖))) = (𝐹‘(𝐴 + (𝐷‘𝐼)))) |
83 | 82 | sneqd 4189 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → {(𝐹‘(𝐴 + (𝐷‘𝑖)))} = {(𝐹‘(𝐴 + (𝐷‘𝐼)))}) |
84 | 83 | imaeq2d 5466 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) = (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝐼)))})) |
85 | 81, 84 | sseq12d 3634 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → (((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) ↔ ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝐼)))}))) |
86 | 85 | rspcv 3305 |
. . . . . . . 8
⊢ (𝐼 ∈ (1...𝑀) → (∀𝑖 ∈ (1...𝑀)((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) → ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝐼)))}))) |
87 | 3, 23, 86 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝐼)))})) |
88 | | vdwlem1.e |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘(𝐴 + (𝐷‘𝐼)))) |
89 | 88 | sneqd 4189 |
. . . . . . . 8
⊢ (𝜑 → {(𝐹‘𝐴)} = {(𝐹‘(𝐴 + (𝐷‘𝐼)))}) |
90 | 89 | imaeq2d 5466 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 “ {(𝐹‘𝐴)}) = (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝐼)))})) |
91 | 87, 90 | sseqtr4d 3642 |
. . . . . 6
⊢ (𝜑 → ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
92 | 78, 91 | unssd 3789 |
. . . . 5
⊢ (𝜑 → ({𝐴} ∪ ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼))) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
93 | 8, 92 | eqsstrd 3639 |
. . . 4
⊢ (𝜑 → (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
94 | | oveq1 6657 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑎(AP‘(𝐾 + 1))𝑑) = (𝐴(AP‘(𝐾 + 1))𝑑)) |
95 | 94 | sseq1d 3632 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ (𝐴(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}))) |
96 | | oveq2 6658 |
. . . . . 6
⊢ (𝑑 = (𝐷‘𝐼) → (𝐴(AP‘(𝐾 + 1))𝑑) = (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼))) |
97 | 96 | sseq1d 3632 |
. . . . 5
⊢ (𝑑 = (𝐷‘𝐼) → ((𝐴(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}))) |
98 | 95, 97 | rspc2ev 3324 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ (𝐷‘𝐼) ∈ ℕ ∧ (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
99 | 1, 4, 93, 98 | syl3anc 1326 |
. . 3
⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
100 | | fvex 6201 |
. . . 4
⊢ (𝐹‘𝐴) ∈ V |
101 | | sneq 4187 |
. . . . . . 7
⊢ (𝑐 = (𝐹‘𝐴) → {𝑐} = {(𝐹‘𝐴)}) |
102 | 101 | imaeq2d 5466 |
. . . . . 6
⊢ (𝑐 = (𝐹‘𝐴) → (◡𝐹 “ {𝑐}) = (◡𝐹 “ {(𝐹‘𝐴)})) |
103 | 102 | sseq2d 3633 |
. . . . 5
⊢ (𝑐 = (𝐹‘𝐴) → ((𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}))) |
104 | 103 | 2rexbidv 3057 |
. . . 4
⊢ (𝑐 = (𝐹‘𝐴) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}))) |
105 | 100, 104 | spcev 3300 |
. . 3
⊢
(∃𝑎 ∈
ℕ ∃𝑑 ∈
ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}) → ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {𝑐})) |
106 | 99, 105 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {𝑐})) |
107 | | ovex 6678 |
. . 3
⊢
(1...𝑊) ∈
V |
108 | | peano2nn0 11333 |
. . . 4
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ0) |
109 | 6, 108 | syl 17 |
. . 3
⊢ (𝜑 → (𝐾 + 1) ∈
ℕ0) |
110 | 107, 109,
26 | vdwmc 15682 |
. 2
⊢ (𝜑 → ((𝐾 + 1) MonoAP 𝐹 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
111 | 106, 110 | mpbird 247 |
1
⊢ (𝜑 → (𝐾 + 1) MonoAP 𝐹) |