Metamath Proof Explorer

Theorem vdwlem12

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

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

Proof

Step Hyp Ref Expression
1 vdw.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
2 vdwlem12.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ⟶ 𝑅 )
3 vdwlem12.2 ⊢ ( 𝜑 → ¬ 2 MonoAP 𝐹 )
4 hashcl ⊢ ( 𝑅 ∈ Fin → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
5 1 4 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) ∈ ℕ0 )
6 5 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) ∈ ℝ )
7 6 ltp1d ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) < ( ( ♯ ‘ 𝑅 ) + 1 ) )
8 nn0p1nn ⊢ ( ( ♯ ‘ 𝑅 ) ∈ ℕ0 → ( ( ♯ ‘ 𝑅 ) + 1 ) ∈ ℕ )
9 5 8 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) + 1 ) ∈ ℕ )
10 9 nnnn0d ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) + 1 ) ∈ ℕ0 )
11 hashfz1 ⊢ ( ( ( ♯ ‘ 𝑅 ) + 1 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) = ( ( ♯ ‘ 𝑅 ) + 1 ) )
12 10 11 syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) = ( ( ♯ ‘ 𝑅 ) + 1 ) )
13 7 12 breqtrrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) < ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) )
14 fzfi ⊢ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∈ Fin
15 hashsdom ⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∈ Fin ) → ( ( ♯ ‘ 𝑅 ) < ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ↔ 𝑅 ≺ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) )
16 1 14 15 sylancl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) < ( ♯ ‘ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ↔ 𝑅 ≺ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) )
17 13 16 mpbid ⊢ ( 𝜑 → 𝑅 ≺ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) )
18 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
19 fveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) )
20 18 19 eqeqan12d ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
21 eqeq12 ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( 𝑧 = 𝑤 ↔ 𝑥 = 𝑦 ) )
22 20 21 imbi12d ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
23 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
24 fveq2 ⊢ ( 𝑤 = 𝑥 → ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑥 ) )
25 23 24 eqeqan12d ⊢ ( ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
26 eqcom ⊢ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
27 25 26 bitrdi ⊢ ( ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
28 eqeq12 ⊢ ( ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( 𝑧 = 𝑤 ↔ 𝑦 = 𝑥 ) )
29 eqcom ⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
30 28 29 bitrdi ⊢ ( ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( 𝑧 = 𝑤 ↔ 𝑥 = 𝑦 ) )
31 27 30 imbi12d ⊢ ( ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) → 𝑧 = 𝑤 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
32 elfznn ⊢ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) → 𝑥 ∈ ℕ )
33 32 nnred ⊢ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) → 𝑥 ∈ ℝ )
34 33 ssriv ⊢ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ⊆ ℝ
35 34 a1i ⊢ ( 𝜑 → ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ⊆ ℝ )
36 biidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
37 simplr3 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ≤ 𝑦 )
38 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ¬ 2 MonoAP 𝐹 )
39 3simpa ⊢ ( ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) → ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) )
40 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) )
41 40 32 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℕ )
42 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 < 𝑦 )
43 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) )
44 elfznn ⊢ ( 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) → 𝑦 ∈ ℕ )
45 43 44 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ℕ )
46 nnsub ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) → ( 𝑥 < 𝑦 ↔ ( 𝑦 − 𝑥 ) ∈ ℕ ) )
47 41 45 46 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑥 < 𝑦 ↔ ( 𝑦 − 𝑥 ) ∈ ℕ ) )
48 42 47 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑦 − 𝑥 ) ∈ ℕ )
49 df-2 ⊢ 2 = ( 1 + 1 )
50 49 fveq2i ⊢ ( AP ‘ 2 ) = ( AP ‘ ( 1 + 1 ) )
51 50 oveqi ⊢ ( 𝑥 ( AP ‘ 2 ) ( 𝑦 − 𝑥 ) ) = ( 𝑥 ( AP ‘ ( 1 + 1 ) ) ( 𝑦 − 𝑥 ) )
52 1nn0 ⊢ 1 ∈ ℕ0
53 vdwapun ⊢ ( ( 1 ∈ ℕ0 ∧ 𝑥 ∈ ℕ ∧ ( 𝑦 − 𝑥 ) ∈ ℕ ) → ( 𝑥 ( AP ‘ ( 1 + 1 ) ) ( 𝑦 − 𝑥 ) ) = ( { 𝑥 } ∪ ( ( 𝑥 + ( 𝑦 − 𝑥 ) ) ( AP ‘ 1 ) ( 𝑦 − 𝑥 ) ) ) )
54 52 41 48 53 mp3an2i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑥 ( AP ‘ ( 1 + 1 ) ) ( 𝑦 − 𝑥 ) ) = ( { 𝑥 } ∪ ( ( 𝑥 + ( 𝑦 − 𝑥 ) ) ( AP ‘ 1 ) ( 𝑦 − 𝑥 ) ) ) )
55 51 54 syl5eq ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑥 ( AP ‘ 2 ) ( 𝑦 − 𝑥 ) ) = ( { 𝑥 } ∪ ( ( 𝑥 + ( 𝑦 − 𝑥 ) ) ( AP ‘ 1 ) ( 𝑦 − 𝑥 ) ) ) )
56 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
57 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝐹 : ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ⟶ 𝑅 )
58 57 ffnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝐹 Fn ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) )
59 fniniseg ⊢ ( 𝐹 Fn ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ↔ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
60 58 59 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ↔ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
61 40 56 60 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
62 61 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → { 𝑥 } ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
63 41 nncnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℂ )
64 45 nncnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ℂ )
65 63 64 pncan3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑥 + ( 𝑦 − 𝑥 ) ) = 𝑦 )
66 65 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( 𝑥 + ( 𝑦 − 𝑥 ) ) ( AP ‘ 1 ) ( 𝑦 − 𝑥 ) ) = ( 𝑦 ( AP ‘ 1 ) ( 𝑦 − 𝑥 ) ) )
67 vdwap1 ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝑦 − 𝑥 ) ∈ ℕ ) → ( 𝑦 ( AP ‘ 1 ) ( 𝑦 − 𝑥 ) ) = { 𝑦 } )
68 45 48 67 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑦 ( AP ‘ 1 ) ( 𝑦 − 𝑥 ) ) = { 𝑦 } )
69 66 68 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( 𝑥 + ( 𝑦 − 𝑥 ) ) ( AP ‘ 1 ) ( 𝑦 − 𝑥 ) ) = { 𝑦 } )
70 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
71 fniniseg ⊢ ( 𝐹 Fn ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) → ( 𝑦 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ↔ ( 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
72 58 71 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑦 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ↔ ( 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) ) )
73 43 70 72 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
74 73 snssd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → { 𝑦 } ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
75 69 74 eqsstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( 𝑥 + ( 𝑦 − 𝑥 ) ) ( AP ‘ 1 ) ( 𝑦 − 𝑥 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
76 62 75 unssd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( { 𝑥 } ∪ ( ( 𝑥 + ( 𝑦 − 𝑥 ) ) ( AP ‘ 1 ) ( 𝑦 − 𝑥 ) ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
77 55 76 eqsstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑥 ( AP ‘ 2 ) ( 𝑦 − 𝑥 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
78 oveq1 ⊢ ( 𝑎 = 𝑥 → ( 𝑎 ( AP ‘ 2 ) 𝑑 ) = ( 𝑥 ( AP ‘ 2 ) 𝑑 ) )
79 78 sseq1d ⊢ ( 𝑎 = 𝑥 → ( ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ↔ ( 𝑥 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) )
80 oveq2 ⊢ ( 𝑑 = ( 𝑦 − 𝑥 ) → ( 𝑥 ( AP ‘ 2 ) 𝑑 ) = ( 𝑥 ( AP ‘ 2 ) ( 𝑦 − 𝑥 ) ) )
81 80 sseq1d ⊢ ( 𝑑 = ( 𝑦 − 𝑥 ) → ( ( 𝑥 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ↔ ( 𝑥 ( AP ‘ 2 ) ( 𝑦 − 𝑥 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) )
82 79 81 rspc2ev ⊢ ( ( 𝑥 ∈ ℕ ∧ ( 𝑦 − 𝑥 ) ∈ ℕ ∧ ( 𝑥 ( AP ‘ 2 ) ( 𝑦 − 𝑥 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
83 41 48 77 82 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
84 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
85 sneq ⊢ ( 𝑐 = ( 𝐹 ‘ 𝑦 ) → { 𝑐 } = { ( 𝐹 ‘ 𝑦 ) } )
86 85 imaeq2d ⊢ ( 𝑐 = ( 𝐹 ‘ 𝑦 ) → ( ◡ 𝐹 “ { 𝑐 } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) )
87 86 sseq2d ⊢ ( 𝑐 = ( 𝐹 ‘ 𝑦 ) → ( ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) )
88 87 2rexbidv ⊢ ( 𝑐 = ( 𝐹 ‘ 𝑦 ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) ) )
89 84 88 spcev ⊢ ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑦 ) } ) → ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
90 83 89 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) )
91 ovex ⊢ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∈ V
92 2nn0 ⊢ 2 ∈ ℕ0
93 92 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 2 ∈ ℕ0 )
94 91 93 57 vdwmc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 2 MonoAP 𝐹 ↔ ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 2 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑐 } ) ) )
95 90 94 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 2 MonoAP 𝐹 )
96 39 95 sylanl2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 2 MonoAP 𝐹 )
97 96 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 < 𝑦 → 2 MonoAP 𝐹 ) )
98 38 97 mtod ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ¬ 𝑥 < 𝑦 )
99 simplr1 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) )
100 99 33 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ ℝ )
101 simplr2 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) )
102 34 101 sseldi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ ℝ )
103 100 102 eqleltd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 = 𝑦 ↔ ( 𝑥 ≤ 𝑦 ∧ ¬ 𝑥 < 𝑦 ) ) )
104 37 98 103 mpbir2and ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
105 104 ex ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑥 ≤ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
106 22 31 35 36 105 wlogle ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∧ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
107 106 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∀ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
108 dff13 ⊢ ( 𝐹 : ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) –1-1→ 𝑅 ↔ ( 𝐹 : ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ⟶ 𝑅 ∧ ∀ 𝑥 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ∀ 𝑦 ∈ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
109 2 107 108 sylanbrc ⊢ ( 𝜑 → 𝐹 : ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) –1-1→ 𝑅 )
110 f1domg ⊢ ( 𝑅 ∈ Fin → ( 𝐹 : ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) –1-1→ 𝑅 → ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ≼ 𝑅 ) )
111 1 109 110 sylc ⊢ ( 𝜑 → ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ≼ 𝑅 )
112 domnsym ⊢ ( ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) ≼ 𝑅 → ¬ 𝑅 ≺ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) )
113 111 112 syl ⊢ ( 𝜑 → ¬ 𝑅 ≺ ( 1 ... ( ( ♯ ‘ 𝑅 ) + 1 ) ) )
114 17 113 pm2.65i ⊢ ¬ 𝜑