Metamath Proof Explorer

Theorem vdwlem13

Description: Lemma for vdw . Main induction on K ; K = 0 , K = 1 base cases. (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdw.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
vdw.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion vdwlem13 ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )

Proof

Step Hyp Ref Expression
1 vdw.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
2 vdw.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 elnn1uz2 ⊢ ( 𝐾 ∈ ℕ ↔ ( 𝐾 = 1 ∨ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) )
4 ovex ⊢ ( 1 ... 1 ) ∈ V
5 elmapg ⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... 1 ) ∈ V ) → ( 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ↔ 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 ) )
6 1 4 5 sylancl ⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ↔ 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 ) )
7 6 biimpa ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ) → 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 )
8 1nn ⊢ 1 ∈ ℕ
9 vdwap1 ⊢ ( ( 1 ∈ ℕ ∧ 1 ∈ ℕ ) → ( 1 ( AP ‘ 1 ) 1 ) = { 1 } )
10 8 8 9 mp2an ⊢ ( 1 ( AP ‘ 1 ) 1 ) = { 1 }
11 1z ⊢ 1 ∈ ℤ
12 elfz3 ⊢ ( 1 ∈ ℤ → 1 ∈ ( 1 ... 1 ) )
13 11 12 mp1i ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 ) → 1 ∈ ( 1 ... 1 ) )
14 eqidd ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 ) → ( 𝑓 ‘ 1 ) = ( 𝑓 ‘ 1 ) )
15 ffn ⊢ ( 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 → 𝑓 Fn ( 1 ... 1 ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 ) → 𝑓 Fn ( 1 ... 1 ) )
17 fniniseg ⊢ ( 𝑓 Fn ( 1 ... 1 ) → ( 1 ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ↔ ( 1 ∈ ( 1 ... 1 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑓 ‘ 1 ) ) ) )
18 16 17 syl ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 ) → ( 1 ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ↔ ( 1 ∈ ( 1 ... 1 ) ∧ ( 𝑓 ‘ 1 ) = ( 𝑓 ‘ 1 ) ) ) )
19 13 14 18 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 ) → 1 ∈ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) )
20 19 snssd ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 ) → { 1 } ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) )
21 10 20 eqsstrid ⊢ ( ( 𝜑 ∧ 𝑓 : ( 1 ... 1 ) ⟶ 𝑅 ) → ( 1 ( AP ‘ 1 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) )
22 7 21 syldan ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ) → ( 1 ( AP ‘ 1 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) )
23 22 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ( 1 ( AP ‘ 1 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) )
24 fveq2 ⊢ ( 𝐾 = 1 → ( AP ‘ 𝐾 ) = ( AP ‘ 1 ) )
25 24 oveqd ⊢ ( 𝐾 = 1 → ( 1 ( AP ‘ 𝐾 ) 1 ) = ( 1 ( AP ‘ 1 ) 1 ) )
26 25 sseq1d ⊢ ( 𝐾 = 1 → ( ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ↔ ( 1 ( AP ‘ 1 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ) )
27 26 ralbidv ⊢ ( 𝐾 = 1 → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ( 1 ( AP ‘ 1 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ) )
28 23 27 syl5ibrcom ⊢ ( 𝜑 → ( 𝐾 = 1 → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ) )
29 oveq1 ⊢ ( 𝑎 = 1 → ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) = ( 1 ( AP ‘ 𝐾 ) 𝑑 ) )
30 29 sseq1d ⊢ ( 𝑎 = 1 → ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ↔ ( 1 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ) )
31 oveq2 ⊢ ( 𝑑 = 1 → ( 1 ( AP ‘ 𝐾 ) 𝑑 ) = ( 1 ( AP ‘ 𝐾 ) 1 ) )
32 31 sseq1d ⊢ ( 𝑑 = 1 → ( ( 1 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ↔ ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ) )
33 30 32 rspc2ev ⊢ ( ( 1 ∈ ℕ ∧ 1 ∈ ℕ ∧ ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ) → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) )
34 8 8 33 mp3an12 ⊢ ( ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) )
35 fvex ⊢ ( 𝑓 ‘ 1 ) ∈ V
36 sneq ⊢ ( 𝑐 = ( 𝑓 ‘ 1 ) → { 𝑐 } = { ( 𝑓 ‘ 1 ) } )
37 36 imaeq2d ⊢ ( 𝑐 = ( 𝑓 ‘ 1 ) → ( ◡ 𝑓 “ { 𝑐 } ) = ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) )
38 37 sseq2d ⊢ ( 𝑐 = ( 𝑓 ‘ 1 ) → ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ) )
39 38 2rexbidv ⊢ ( 𝑐 = ( 𝑓 ‘ 1 ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) ) )
40 35 39 spcev ⊢ ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) → ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) )
41 34 40 syl ⊢ ( ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) → ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) )
42 2 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ) → 𝐾 ∈ ℕ0 )
43 4 42 7 vdwmc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ) → ( 𝐾 MonoAP 𝑓 ↔ ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝑓 “ { 𝑐 } ) ) )
44 41 43 imbitrrid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ) → ( ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) → 𝐾 MonoAP 𝑓 ) )
45 44 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) 𝐾 MonoAP 𝑓 ) )
46 oveq2 ⊢ ( 𝑛 = 1 → ( 1 ... 𝑛 ) = ( 1 ... 1 ) )
47 46 oveq2d ⊢ ( 𝑛 = 1 → ( 𝑅 ↑m ( 1 ... 𝑛 ) ) = ( 𝑅 ↑m ( 1 ... 1 ) ) )
48 47 raleqdv ⊢ ( 𝑛 = 1 → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) 𝐾 MonoAP 𝑓 ) )
49 48 rspcev ⊢ ( ( 1 ∈ ℕ ∧ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) 𝐾 MonoAP 𝑓 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
50 8 49 mpan ⊢ ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) 𝐾 MonoAP 𝑓 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
51 45 50 syl6 ⊢ ( 𝜑 → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
52 28 51 syld ⊢ ( 𝜑 → ( 𝐾 = 1 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
53 breq1 ⊢ ( 𝑥 = 2 → ( 𝑥 MonoAP 𝑓 ↔ 2 MonoAP 𝑓 ) )
54 53 rexralbidv ⊢ ( 𝑥 = 2 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑥 MonoAP 𝑓 ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 2 MonoAP 𝑓 ) )
55 54 ralbidv ⊢ ( 𝑥 = 2 → ( ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑥 MonoAP 𝑓 ↔ ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 2 MonoAP 𝑓 ) )
56 breq1 ⊢ ( 𝑥 = 𝑘 → ( 𝑥 MonoAP 𝑓 ↔ 𝑘 MonoAP 𝑓 ) )
57 56 rexralbidv ⊢ ( 𝑥 = 𝑘 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑥 MonoAP 𝑓 ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ) )
58 57 ralbidv ⊢ ( 𝑥 = 𝑘 → ( ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑥 MonoAP 𝑓 ↔ ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ) )
59 breq1 ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( 𝑥 MonoAP 𝑓 ↔ ( 𝑘 + 1 ) MonoAP 𝑓 ) )
60 59 rexralbidv ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑥 MonoAP 𝑓 ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) ( 𝑘 + 1 ) MonoAP 𝑓 ) )
61 60 ralbidv ⊢ ( 𝑥 = ( 𝑘 + 1 ) → ( ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑥 MonoAP 𝑓 ↔ ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) ( 𝑘 + 1 ) MonoAP 𝑓 ) )
62 breq1 ⊢ ( 𝑥 = 𝐾 → ( 𝑥 MonoAP 𝑓 ↔ 𝐾 MonoAP 𝑓 ) )
63 62 rexralbidv ⊢ ( 𝑥 = 𝐾 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑥 MonoAP 𝑓 ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
64 63 ralbidv ⊢ ( 𝑥 = 𝐾 → ( ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑥 MonoAP 𝑓 ↔ ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
65 hashcl ⊢ ( 𝑟 ∈ Fin → ( ♯ ‘ 𝑟 ) ∈ ℕ0 )
66 nn0p1nn ⊢ ( ( ♯ ‘ 𝑟 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑟 ) + 1 ) ∈ ℕ )
67 65 66 syl ⊢ ( 𝑟 ∈ Fin → ( ( ♯ ‘ 𝑟 ) + 1 ) ∈ ℕ )
68 simpll ⊢ ( ( ( 𝑟 ∈ Fin ∧ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) ) ∧ ¬ 2 MonoAP 𝑓 ) → 𝑟 ∈ Fin )
69 simplr ⊢ ( ( ( 𝑟 ∈ Fin ∧ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) ) ∧ ¬ 2 MonoAP 𝑓 ) → 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) )
70 vex ⊢ 𝑟 ∈ V
71 ovex ⊢ ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ∈ V
72 70 71 elmap ⊢ ( 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) ↔ 𝑓 : ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ⟶ 𝑟 )
73 69 72 sylib ⊢ ( ( ( 𝑟 ∈ Fin ∧ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) ) ∧ ¬ 2 MonoAP 𝑓 ) → 𝑓 : ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ⟶ 𝑟 )
74 simpr ⊢ ( ( ( 𝑟 ∈ Fin ∧ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) ) ∧ ¬ 2 MonoAP 𝑓 ) → ¬ 2 MonoAP 𝑓 )
75 68 73 74 vdwlem12 ⊢ ¬ ( ( 𝑟 ∈ Fin ∧ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) ) ∧ ¬ 2 MonoAP 𝑓 )
76 iman ⊢ ( ( ( 𝑟 ∈ Fin ∧ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) ) → 2 MonoAP 𝑓 ) ↔ ¬ ( ( 𝑟 ∈ Fin ∧ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) ) ∧ ¬ 2 MonoAP 𝑓 ) )
77 75 76 mpbir ⊢ ( ( 𝑟 ∈ Fin ∧ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) ) → 2 MonoAP 𝑓 )
78 77 ralrimiva ⊢ ( 𝑟 ∈ Fin → ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) 2 MonoAP 𝑓 )
79 oveq2 ⊢ ( 𝑛 = ( ( ♯ ‘ 𝑟 ) + 1 ) → ( 1 ... 𝑛 ) = ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) )
80 79 oveq2d ⊢ ( 𝑛 = ( ( ♯ ‘ 𝑟 ) + 1 ) → ( 𝑟 ↑m ( 1 ... 𝑛 ) ) = ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) )
81 80 raleqdv ⊢ ( 𝑛 = ( ( ♯ ‘ 𝑟 ) + 1 ) → ( ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 2 MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) 2 MonoAP 𝑓 ) )
82 81 rspcev ⊢ ( ( ( ( ♯ ‘ 𝑟 ) + 1 ) ∈ ℕ ∧ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... ( ( ♯ ‘ 𝑟 ) + 1 ) ) ) 2 MonoAP 𝑓 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 2 MonoAP 𝑓 )
83 67 78 82 syl2anc ⊢ ( 𝑟 ∈ Fin → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 2 MonoAP 𝑓 )
84 83 rgen ⊢ ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 2 MonoAP 𝑓
85 oveq1 ⊢ ( 𝑟 = 𝑠 → ( 𝑟 ↑m ( 1 ... 𝑛 ) ) = ( 𝑠 ↑m ( 1 ... 𝑛 ) ) )
86 85 raleqdv ⊢ ( 𝑟 = 𝑠 → ( ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ) )
87 86 rexbidv ⊢ ( 𝑟 = 𝑠 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ) )
88 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 1 ... 𝑛 ) = ( 1 ... 𝑚 ) )
89 88 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑠 ↑m ( 1 ... 𝑛 ) ) = ( 𝑠 ↑m ( 1 ... 𝑚 ) ) )
90 89 raleqdv ⊢ ( 𝑛 = 𝑚 → ( ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑓 ) )
91 breq2 ⊢ ( 𝑓 = 𝑔 → ( 𝑘 MonoAP 𝑓 ↔ 𝑘 MonoAP 𝑔 ) )
92 91 cbvralvw ⊢ ( ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑓 ↔ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 )
93 90 92 bitrdi ⊢ ( 𝑛 = 𝑚 → ( ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ↔ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 ) )
94 93 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ↔ ∃ 𝑚 ∈ ℕ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 )
95 87 94 bitrdi ⊢ ( 𝑟 = 𝑠 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ↔ ∃ 𝑚 ∈ ℕ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 ) )
96 95 cbvralvw ⊢ ( ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ↔ ∀ 𝑠 ∈ Fin ∃ 𝑚 ∈ ℕ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 )
97 simplr ⊢ ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑟 ∈ Fin ) ∧ ∀ 𝑠 ∈ Fin ∃ 𝑚 ∈ ℕ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 ) → 𝑟 ∈ Fin )
98 simpll ⊢ ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑟 ∈ Fin ) ∧ ∀ 𝑠 ∈ Fin ∃ 𝑚 ∈ ℕ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 ) → 𝑘 ∈ ( ℤ≥ ‘ 2 ) )
99 94 ralbii ⊢ ( ∀ 𝑠 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 ↔ ∀ 𝑠 ∈ Fin ∃ 𝑚 ∈ ℕ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 )
100 99 bilanri ⊢ ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑟 ∈ Fin ) ∧ ∀ 𝑠 ∈ Fin ∃ 𝑚 ∈ ℕ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 ) → ∀ 𝑠 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 )
101 97 98 100 vdwlem11 ⊢ ( ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑟 ∈ Fin ) ∧ ∀ 𝑠 ∈ Fin ∃ 𝑚 ∈ ℕ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) ( 𝑘 + 1 ) MonoAP 𝑓 )
102 101 ex ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑟 ∈ Fin ) → ( ∀ 𝑠 ∈ Fin ∃ 𝑚 ∈ ℕ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) ( 𝑘 + 1 ) MonoAP 𝑓 ) )
103 102 ralrimdva ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑠 ∈ Fin ∃ 𝑚 ∈ ℕ ∀ 𝑔 ∈ ( 𝑠 ↑m ( 1 ... 𝑚 ) ) 𝑘 MonoAP 𝑔 → ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) ( 𝑘 + 1 ) MonoAP 𝑓 ) )
104 96 103 biimtrid ⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝑘 MonoAP 𝑓 → ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) ( 𝑘 + 1 ) MonoAP 𝑓 ) )
105 55 58 61 64 84 104 uzind4i ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
106 oveq1 ⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑m ( 1 ... 𝑛 ) ) = ( 𝑅 ↑m ( 1 ... 𝑛 ) ) )
107 106 raleqdv ⊢ ( 𝑟 = 𝑅 → ( ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
108 107 rexbidv ⊢ ( 𝑟 = 𝑅 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
109 108 rspcv ⊢ ( 𝑅 ∈ Fin → ( ∀ 𝑟 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑟 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
110 1 105 109 syl2im ⊢ ( 𝜑 → ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
111 52 110 jaod ⊢ ( 𝜑 → ( ( 𝐾 = 1 ∨ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
112 3 111 biimtrid ⊢ ( 𝜑 → ( 𝐾 ∈ ℕ → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
113 fveq2 ⊢ ( 𝐾 = 0 → ( AP ‘ 𝐾 ) = ( AP ‘ 0 ) )
114 113 oveqd ⊢ ( 𝐾 = 0 → ( 1 ( AP ‘ 𝐾 ) 1 ) = ( 1 ( AP ‘ 0 ) 1 ) )
115 vdwap0 ⊢ ( ( 1 ∈ ℕ ∧ 1 ∈ ℕ ) → ( 1 ( AP ‘ 0 ) 1 ) = ∅ )
116 8 8 115 mp2an ⊢ ( 1 ( AP ‘ 0 ) 1 ) = ∅
117 114 116 eqtrdi ⊢ ( 𝐾 = 0 → ( 1 ( AP ‘ 𝐾 ) 1 ) = ∅ )
118 0ss ⊢ ∅ ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } )
119 117 118 eqsstrdi ⊢ ( 𝐾 = 0 → ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) )
120 119 ralrimivw ⊢ ( 𝐾 = 0 → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 1 ) ) ( 1 ( AP ‘ 𝐾 ) 1 ) ⊆ ( ◡ 𝑓 “ { ( 𝑓 ‘ 1 ) } ) )
121 120 51 syl5 ⊢ ( 𝜑 → ( 𝐾 = 0 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
122 elnn0 ⊢ ( 𝐾 ∈ ℕ0 ↔ ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) )
123 2 122 sylib ⊢ ( 𝜑 → ( 𝐾 ∈ ℕ ∨ 𝐾 = 0 ) )
124 112 121 123 mpjaod ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )