Metamath Proof Explorer

Theorem vdwlem1

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses vdwlem1.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
vdwlem1.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
vdwlem1.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
vdwlem1.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
vdwlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
vdwlem1.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
vdwlem1.d ⊢ ( 𝜑 → 𝐷 : ( 1 ... 𝑀 ) ⟶ ℕ )
vdwlem1.s ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ) } ) )
vdwlem1.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑀 ) )
vdwlem1.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ) )
Assertion vdwlem1 ( 𝜑 → ( 𝐾 + 1 ) MonoAP 𝐹 )

Proof

Step Hyp Ref Expression
1 vdwlem1.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
2 vdwlem1.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 vdwlem1.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
4 vdwlem1.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
5 vdwlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
6 vdwlem1.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7 vdwlem1.d ⊢ ( 𝜑 → 𝐷 : ( 1 ... 𝑀 ) ⟶ ℕ )
8 vdwlem1.s ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ) } ) )
9 vdwlem1.i ⊢ ( 𝜑 → 𝐼 ∈ ( 1 ... 𝑀 ) )
10 vdwlem1.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ) )
11 7 9 ffvelrnd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐼 ) ∈ ℕ )
12 2 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
13 vdwapun ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ ( 𝐷 ‘ 𝐼 ) ∈ ℕ ) → ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) ( 𝐷 ‘ 𝐼 ) ) = ( { 𝐴 } ∪ ( ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝐼 ) ) ) )
14 12 5 11 13 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) ( 𝐷 ‘ 𝐼 ) ) = ( { 𝐴 } ∪ ( ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝐼 ) ) ) )
15 5 nnred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
16 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
17 6 16 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
18 eluzfz1 ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑀 ) )
19 17 18 syl ⊢ ( 𝜑 → 1 ∈ ( 1 ... 𝑀 ) )
20 7 19 ffvelrnd ⊢ ( 𝜑 → ( 𝐷 ‘ 1 ) ∈ ℕ )
21 5 20 nnaddcld ⊢ ( 𝜑 → ( 𝐴 + ( 𝐷 ‘ 1 ) ) ∈ ℕ )
22 21 nnred ⊢ ( 𝜑 → ( 𝐴 + ( 𝐷 ‘ 1 ) ) ∈ ℝ )
23 3 nnred ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
24 20 nnrpd ⊢ ( 𝜑 → ( 𝐷 ‘ 1 ) ∈ ℝ+ )
25 15 24 ltaddrpd ⊢ ( 𝜑 → 𝐴 < ( 𝐴 + ( 𝐷 ‘ 1 ) ) )
26 15 22 25 ltled ⊢ ( 𝜑 → 𝐴 ≤ ( 𝐴 + ( 𝐷 ‘ 1 ) ) )
27 fveq2 ⊢ ( 𝑖 = 1 → ( 𝐷 ‘ 𝑖 ) = ( 𝐷 ‘ 1 ) )
28 27 oveq2d ⊢ ( 𝑖 = 1 → ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) = ( 𝐴 + ( 𝐷 ‘ 1 ) ) )
29 28 eleq1d ⊢ ( 𝑖 = 1 → ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ∈ ( 1 ... 𝑊 ) ↔ ( 𝐴 + ( 𝐷 ‘ 1 ) ) ∈ ( 1 ... 𝑊 ) ) )
30 8 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ) } ) )
31 cnvimass ⊢ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ) } ) ⊆ dom 𝐹
32 31 4 fssdm ⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ) } ) ⊆ ( 1 ... 𝑊 ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ) } ) ⊆ ( 1 ... 𝑊 ) )
34 30 33 sstrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( 1 ... 𝑊 ) )
35 nnm1nn0 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
36 2 35 syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ0 )
37 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
38 36 37 eleqtrdi ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 0 ) )
39 eluzfz1 ⊢ ( ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 0 ) → 0 ∈ ( 0 ... ( 𝐾 − 1 ) ) )
40 38 39 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... ( 𝐾 − 1 ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 0 ∈ ( 0 ... ( 𝐾 − 1 ) ) )
42 7 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑖 ) ∈ ℕ )
43 42 nncnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐷 ‘ 𝑖 ) ∈ ℂ )
44 43 mul02d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 0 · ( 𝐷 ‘ 𝑖 ) ) = 0 )
45 44 oveq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + ( 0 · ( 𝐷 ‘ 𝑖 ) ) ) = ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + 0 ) )
46 5 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝐴 ∈ ℕ )
47 46 42 nnaddcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ∈ ℕ )
48 47 nncnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ∈ ℂ )
49 48 addid1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + 0 ) = ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) )
50 45 49 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) = ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + ( 0 · ( 𝐷 ‘ 𝑖 ) ) ) )
51 oveq1 ⊢ ( 𝑚 = 0 → ( 𝑚 · ( 𝐷 ‘ 𝑖 ) ) = ( 0 · ( 𝐷 ‘ 𝑖 ) ) )
52 51 oveq2d ⊢ ( 𝑚 = 0 → ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝐷 ‘ 𝑖 ) ) ) = ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + ( 0 · ( 𝐷 ‘ 𝑖 ) ) ) )
53 52 rspceeqv ⊢ ( ( 0 ∈ ( 0 ... ( 𝐾 − 1 ) ) ∧ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) = ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + ( 0 · ( 𝐷 ‘ 𝑖 ) ) ) ) → ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) = ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝐷 ‘ 𝑖 ) ) ) )
54 41 50 53 syl2anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) = ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝐷 ‘ 𝑖 ) ) ) )
55 2 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝐾 ∈ ℕ )
56 55 nnnn0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → 𝐾 ∈ ℕ0 )
57 vdwapval ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ∈ ℕ ∧ ( 𝐷 ‘ 𝑖 ) ∈ ℕ ) → ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ∈ ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝑖 ) ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) = ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝐷 ‘ 𝑖 ) ) ) ) )
58 56 47 42 57 syl3anc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ∈ ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝑖 ) ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) = ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) + ( 𝑚 · ( 𝐷 ‘ 𝑖 ) ) ) ) )
59 54 58 mpbird ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ∈ ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝑖 ) ) )
60 34 59 sseldd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑀 ) ) → ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ∈ ( 1 ... 𝑊 ) )
61 60 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ∈ ( 1 ... 𝑊 ) )
62 29 61 19 rspcdva ⊢ ( 𝜑 → ( 𝐴 + ( 𝐷 ‘ 1 ) ) ∈ ( 1 ... 𝑊 ) )
63 elfzle2 ⊢ ( ( 𝐴 + ( 𝐷 ‘ 1 ) ) ∈ ( 1 ... 𝑊 ) → ( 𝐴 + ( 𝐷 ‘ 1 ) ) ≤ 𝑊 )
64 62 63 syl ⊢ ( 𝜑 → ( 𝐴 + ( 𝐷 ‘ 1 ) ) ≤ 𝑊 )
65 15 22 23 26 64 letrd ⊢ ( 𝜑 → 𝐴 ≤ 𝑊 )
66 5 16 eleqtrdi ⊢ ( 𝜑 → 𝐴 ∈ ( ℤ≥ ‘ 1 ) )
67 3 nnzd ⊢ ( 𝜑 → 𝑊 ∈ ℤ )
68 elfz5 ⊢ ( ( 𝐴 ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑊 ∈ ℤ ) → ( 𝐴 ∈ ( 1 ... 𝑊 ) ↔ 𝐴 ≤ 𝑊 ) )
69 66 67 68 syl2anc ⊢ ( 𝜑 → ( 𝐴 ∈ ( 1 ... 𝑊 ) ↔ 𝐴 ≤ 𝑊 ) )
70 65 69 mpbird ⊢ ( 𝜑 → 𝐴 ∈ ( 1 ... 𝑊 ) )
71 eqidd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
72 ffn ⊢ ( 𝐹 : ( 1 ... 𝑊 ) ⟶ 𝑅 → 𝐹 Fn ( 1 ... 𝑊 ) )
73 fniniseg ⊢ ( 𝐹 Fn ( 1 ... 𝑊 ) → ( 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ↔ ( 𝐴 ∈ ( 1 ... 𝑊 ) ∧ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) ) )
74 4 72 73 3syl ⊢ ( 𝜑 → ( 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ↔ ( 𝐴 ∈ ( 1 ... 𝑊 ) ∧ ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) ) )
75 70 71 74 mpbir2and ⊢ ( 𝜑 → 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) )
76 75 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) )
77 fveq2 ⊢ ( 𝑖 = 𝐼 → ( 𝐷 ‘ 𝑖 ) = ( 𝐷 ‘ 𝐼 ) )
78 77 oveq2d ⊢ ( 𝑖 = 𝐼 → ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) = ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) )
79 78 77 oveq12d ⊢ ( 𝑖 = 𝐼 → ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝑖 ) ) = ( ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝐼 ) ) )
80 78 fveq2d ⊢ ( 𝑖 = 𝐼 → ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ) )
81 80 sneqd ⊢ ( 𝑖 = 𝐼 → { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ) } = { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ) } )
82 81 imaeq2d ⊢ ( 𝑖 = 𝐼 → ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ) } ) )
83 79 82 sseq12d ⊢ ( 𝑖 = 𝐼 → ( ( ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝑖 ) ) ) } ) ↔ ( ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝐼 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ) } ) ) )
84 83 8 9 rspcdva ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝐼 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ) } ) )
85 10 sneqd ⊢ ( 𝜑 → { ( 𝐹 ‘ 𝐴 ) } = { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ) } )
86 85 imaeq2d ⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ) } ) )
87 84 86 sseqtrrd ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝐼 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) )
88 76 87 unssd ⊢ ( 𝜑 → ( { 𝐴 } ∪ ( ( 𝐴 + ( 𝐷 ‘ 𝐼 ) ) ( AP ‘ 𝐾 ) ( 𝐷 ‘ 𝐼 ) ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) )
89 14 88 eqsstrd ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) ( 𝐷 ‘ 𝐼 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) )
90 oveq1 ⊢ ( 𝑎 = 𝐴 → ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) = ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) )
91 90 sseq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ↔ ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ) )
92 oveq2 ⊢ ( 𝑑 = ( 𝐷 ‘ 𝐼 ) → ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) = ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) ( 𝐷 ‘ 𝐼 ) ) )
93 92 sseq1d ⊢ ( 𝑑 = ( 𝐷 ‘ 𝐼 ) → ( ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ↔ ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) ( 𝐷 ‘ 𝐼 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ) )
94 91 93 rspc2ev ⊢ ( ( 𝐴 ∈ ℕ ∧ ( 𝐷 ‘ 𝐼 ) ∈ ℕ ∧ ( 𝐴 ( AP ‘ ( 𝐾 + 1 ) ) ( 𝐷 ‘ 𝐼 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ) → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) )
95 5 11 89 94 syl3anc ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) )
96 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
97 sneq ⊢ ( 𝑐 = ( 𝐹 ‘ 𝐴 ) → { 𝑐 } = { ( 𝐹 ‘ 𝐴 ) } )
98 97 imaeq2d ⊢ ( 𝑐 = ( 𝐹 ‘ 𝐴 ) → ( ◡ 𝐹 “ { 𝑐 } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) )
99 98 sseq2d ⊢ ( 𝑐 = ( 𝐹 ‘ 𝐴 ) → ( ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ) )
100 99 2rexbidv ⊢ ( 𝑐 = ( 𝐹 ‘ 𝐴 ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ) )
101 96 100 spcev ⊢ ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) → ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
102 95 101 syl ⊢ ( 𝜑 → ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
103 ovex ⊢ ( 1 ... 𝑊 ) ∈ V
104 peano2nn0 ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ0 )
105 12 104 syl ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℕ0 )
106 103 105 4 vdwmc ⊢ ( 𝜑 → ( ( 𝐾 + 1 ) MonoAP 𝐹 ↔ ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ ( 𝐾 + 1 ) ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
107 102 106 mpbird ⊢ ( 𝜑 → ( 𝐾 + 1 ) MonoAP 𝐹 )