# 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 ${⊢}{\phi }\to {R}\in \mathrm{Fin}$
vdwlem12.f ${⊢}{\phi }\to {F}:\left(1\dots \left|{R}\right|+1\right)⟶{R}$
vdwlem12.2 ${⊢}{\phi }\to ¬2\mathrm{MonoAP}{F}$
Assertion vdwlem12 ${⊢}¬{\phi }$

### Proof

Step Hyp Ref Expression
1 vdw.r ${⊢}{\phi }\to {R}\in \mathrm{Fin}$
2 vdwlem12.f ${⊢}{\phi }\to {F}:\left(1\dots \left|{R}\right|+1\right)⟶{R}$
3 vdwlem12.2 ${⊢}{\phi }\to ¬2\mathrm{MonoAP}{F}$
4 hashcl ${⊢}{R}\in \mathrm{Fin}\to \left|{R}\right|\in {ℕ}_{0}$
5 1 4 syl ${⊢}{\phi }\to \left|{R}\right|\in {ℕ}_{0}$
6 5 nn0red ${⊢}{\phi }\to \left|{R}\right|\in ℝ$
7 6 ltp1d ${⊢}{\phi }\to \left|{R}\right|<\left|{R}\right|+1$
8 nn0p1nn ${⊢}\left|{R}\right|\in {ℕ}_{0}\to \left|{R}\right|+1\in ℕ$
9 5 8 syl ${⊢}{\phi }\to \left|{R}\right|+1\in ℕ$
10 9 nnnn0d ${⊢}{\phi }\to \left|{R}\right|+1\in {ℕ}_{0}$
11 hashfz1 ${⊢}\left|{R}\right|+1\in {ℕ}_{0}\to \left|\left(1\dots \left|{R}\right|+1\right)\right|=\left|{R}\right|+1$
12 10 11 syl ${⊢}{\phi }\to \left|\left(1\dots \left|{R}\right|+1\right)\right|=\left|{R}\right|+1$
13 7 12 breqtrrd ${⊢}{\phi }\to \left|{R}\right|<\left|\left(1\dots \left|{R}\right|+1\right)\right|$
14 fzfi ${⊢}\left(1\dots \left|{R}\right|+1\right)\in \mathrm{Fin}$
15 hashsdom ${⊢}\left({R}\in \mathrm{Fin}\wedge \left(1\dots \left|{R}\right|+1\right)\in \mathrm{Fin}\right)\to \left(\left|{R}\right|<\left|\left(1\dots \left|{R}\right|+1\right)\right|↔{R}\prec \left(1\dots \left|{R}\right|+1\right)\right)$
16 1 14 15 sylancl ${⊢}{\phi }\to \left(\left|{R}\right|<\left|\left(1\dots \left|{R}\right|+1\right)\right|↔{R}\prec \left(1\dots \left|{R}\right|+1\right)\right)$
17 13 16 mpbid ${⊢}{\phi }\to {R}\prec \left(1\dots \left|{R}\right|+1\right)$
18 fveq2 ${⊢}{z}={x}\to {F}\left({z}\right)={F}\left({x}\right)$
19 fveq2 ${⊢}{w}={y}\to {F}\left({w}\right)={F}\left({y}\right)$
20 18 19 eqeqan12d ${⊢}\left({z}={x}\wedge {w}={y}\right)\to \left({F}\left({z}\right)={F}\left({w}\right)↔{F}\left({x}\right)={F}\left({y}\right)\right)$
21 eqeq12 ${⊢}\left({z}={x}\wedge {w}={y}\right)\to \left({z}={w}↔{x}={y}\right)$
22 20 21 imbi12d ${⊢}\left({z}={x}\wedge {w}={y}\right)\to \left(\left({F}\left({z}\right)={F}\left({w}\right)\to {z}={w}\right)↔\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
23 fveq2 ${⊢}{z}={y}\to {F}\left({z}\right)={F}\left({y}\right)$
24 fveq2 ${⊢}{w}={x}\to {F}\left({w}\right)={F}\left({x}\right)$
25 23 24 eqeqan12d ${⊢}\left({z}={y}\wedge {w}={x}\right)\to \left({F}\left({z}\right)={F}\left({w}\right)↔{F}\left({y}\right)={F}\left({x}\right)\right)$
26 eqcom ${⊢}{F}\left({y}\right)={F}\left({x}\right)↔{F}\left({x}\right)={F}\left({y}\right)$
27 25 26 syl6bb ${⊢}\left({z}={y}\wedge {w}={x}\right)\to \left({F}\left({z}\right)={F}\left({w}\right)↔{F}\left({x}\right)={F}\left({y}\right)\right)$
28 eqeq12 ${⊢}\left({z}={y}\wedge {w}={x}\right)\to \left({z}={w}↔{y}={x}\right)$
29 eqcom ${⊢}{y}={x}↔{x}={y}$
30 28 29 syl6bb ${⊢}\left({z}={y}\wedge {w}={x}\right)\to \left({z}={w}↔{x}={y}\right)$
31 27 30 imbi12d ${⊢}\left({z}={y}\wedge {w}={x}\right)\to \left(\left({F}\left({z}\right)={F}\left({w}\right)\to {z}={w}\right)↔\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
32 elfznn ${⊢}{x}\in \left(1\dots \left|{R}\right|+1\right)\to {x}\in ℕ$
33 32 nnred ${⊢}{x}\in \left(1\dots \left|{R}\right|+1\right)\to {x}\in ℝ$
34 33 ssriv ${⊢}\left(1\dots \left|{R}\right|+1\right)\subseteq ℝ$
35 34 a1i ${⊢}{\phi }\to \left(1\dots \left|{R}\right|+1\right)\subseteq ℝ$
36 biidd ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\to \left(\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)↔\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
37 simplr3 ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to {x}\le {y}$
38 3 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to ¬2\mathrm{MonoAP}{F}$
39 3simpa ${⊢}\left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\to \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)$
40 simplrl ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {x}\in \left(1\dots \left|{R}\right|+1\right)$
41 40 32 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {x}\in ℕ$
42 simprr ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {x}<{y}$
43 simplrr ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {y}\in \left(1\dots \left|{R}\right|+1\right)$
44 elfznn ${⊢}{y}\in \left(1\dots \left|{R}\right|+1\right)\to {y}\in ℕ$
45 43 44 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {y}\in ℕ$
46 nnsub ${⊢}\left({x}\in ℕ\wedge {y}\in ℕ\right)\to \left({x}<{y}↔{y}-{x}\in ℕ\right)$
47 41 45 46 syl2anc ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \left({x}<{y}↔{y}-{x}\in ℕ\right)$
48 42 47 mpbid ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {y}-{x}\in ℕ$
49 df-2 ${⊢}2=1+1$
50 49 fveq2i ${⊢}\mathrm{AP}\left(2\right)=\mathrm{AP}\left(1+1\right)$
51 50 oveqi ${⊢}{x}\mathrm{AP}\left(2\right)\left({y}-{x}\right)={x}\mathrm{AP}\left(1+1\right)\left({y}-{x}\right)$
52 1nn0 ${⊢}1\in {ℕ}_{0}$
53 vdwapun ${⊢}\left(1\in {ℕ}_{0}\wedge {x}\in ℕ\wedge {y}-{x}\in ℕ\right)\to {x}\mathrm{AP}\left(1+1\right)\left({y}-{x}\right)=\left\{{x}\right\}\cup \left(\left({x}+{y}-{x}\right)\mathrm{AP}\left(1\right)\left({y}-{x}\right)\right)$
54 52 41 48 53 mp3an2i ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {x}\mathrm{AP}\left(1+1\right)\left({y}-{x}\right)=\left\{{x}\right\}\cup \left(\left({x}+{y}-{x}\right)\mathrm{AP}\left(1\right)\left({y}-{x}\right)\right)$
55 51 54 syl5eq ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {x}\mathrm{AP}\left(2\right)\left({y}-{x}\right)=\left\{{x}\right\}\cup \left(\left({x}+{y}-{x}\right)\mathrm{AP}\left(1\right)\left({y}-{x}\right)\right)$
56 simprl ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {F}\left({x}\right)={F}\left({y}\right)$
57 2 ad2antrr ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {F}:\left(1\dots \left|{R}\right|+1\right)⟶{R}$
58 57 ffnd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {F}Fn\left(1\dots \left|{R}\right|+1\right)$
59 fniniseg ${⊢}{F}Fn\left(1\dots \left|{R}\right|+1\right)\to \left({x}\in {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]↔\left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\right)$
60 58 59 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \left({x}\in {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]↔\left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\right)$
61 40 56 60 mpbir2and ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {x}\in {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]$
62 61 snssd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \left\{{x}\right\}\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]$
63 41 nncnd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {x}\in ℂ$
64 45 nncnd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {y}\in ℂ$
65 63 64 pncan3d ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {x}+{y}-{x}={y}$
66 65 oveq1d ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \left({x}+{y}-{x}\right)\mathrm{AP}\left(1\right)\left({y}-{x}\right)={y}\mathrm{AP}\left(1\right)\left({y}-{x}\right)$
67 vdwap1 ${⊢}\left({y}\in ℕ\wedge {y}-{x}\in ℕ\right)\to {y}\mathrm{AP}\left(1\right)\left({y}-{x}\right)=\left\{{y}\right\}$
68 45 48 67 syl2anc ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {y}\mathrm{AP}\left(1\right)\left({y}-{x}\right)=\left\{{y}\right\}$
69 66 68 eqtrd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \left({x}+{y}-{x}\right)\mathrm{AP}\left(1\right)\left({y}-{x}\right)=\left\{{y}\right\}$
70 eqidd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {F}\left({y}\right)={F}\left({y}\right)$
71 fniniseg ${⊢}{F}Fn\left(1\dots \left|{R}\right|+1\right)\to \left({y}\in {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]↔\left({y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {F}\left({y}\right)={F}\left({y}\right)\right)\right)$
72 58 71 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \left({y}\in {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]↔\left({y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {F}\left({y}\right)={F}\left({y}\right)\right)\right)$
73 43 70 72 mpbir2and ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {y}\in {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]$
74 73 snssd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \left\{{y}\right\}\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]$
75 69 74 eqsstrd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \left({x}+{y}-{x}\right)\mathrm{AP}\left(1\right)\left({y}-{x}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]$
76 62 75 unssd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \left\{{x}\right\}\cup \left(\left({x}+{y}-{x}\right)\mathrm{AP}\left(1\right)\left({y}-{x}\right)\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]$
77 55 76 eqsstrd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to {x}\mathrm{AP}\left(2\right)\left({y}-{x}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]$
78 oveq1 ${⊢}{a}={x}\to {a}\mathrm{AP}\left(2\right){d}={x}\mathrm{AP}\left(2\right){d}$
79 78 sseq1d ${⊢}{a}={x}\to \left({a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]↔{x}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]\right)$
80 oveq2 ${⊢}{d}={y}-{x}\to {x}\mathrm{AP}\left(2\right){d}={x}\mathrm{AP}\left(2\right)\left({y}-{x}\right)$
81 80 sseq1d ${⊢}{d}={y}-{x}\to \left({x}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]↔{x}\mathrm{AP}\left(2\right)\left({y}-{x}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]\right)$
82 79 81 rspc2ev ${⊢}\left({x}\in ℕ\wedge {y}-{x}\in ℕ\wedge {x}\mathrm{AP}\left(2\right)\left({y}-{x}\right)\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]\right)\to \exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]$
83 41 48 77 82 syl3anc ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]$
84 fvex ${⊢}{F}\left({y}\right)\in \mathrm{V}$
85 sneq ${⊢}{c}={F}\left({y}\right)\to \left\{{c}\right\}=\left\{{F}\left({y}\right)\right\}$
86 85 imaeq2d ${⊢}{c}={F}\left({y}\right)\to {{F}}^{-1}\left[\left\{{c}\right\}\right]={{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]$
87 86 sseq2d ${⊢}{c}={F}\left({y}\right)\to \left({a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{c}\right\}\right]↔{a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]\right)$
88 87 2rexbidv ${⊢}{c}={F}\left({y}\right)\to \left(\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{c}\right\}\right]↔\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]\right)$
89 84 88 spcev ${⊢}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{F}\left({y}\right)\right\}\right]\to \exists {c}\phantom{\rule{.4em}{0ex}}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{c}\right\}\right]$
90 83 89 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \exists {c}\phantom{\rule{.4em}{0ex}}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{c}\right\}\right]$
91 ovex ${⊢}\left(1\dots \left|{R}\right|+1\right)\in \mathrm{V}$
92 2nn0 ${⊢}2\in {ℕ}_{0}$
93 92 a1i ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to 2\in {ℕ}_{0}$
94 91 93 57 vdwmc ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to \left(2\mathrm{MonoAP}{F}↔\exists {c}\phantom{\rule{.4em}{0ex}}\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in ℕ\phantom{\rule{.4em}{0ex}}{a}\mathrm{AP}\left(2\right){d}\subseteq {{F}}^{-1}\left[\left\{{c}\right\}\right]\right)$
95 90 94 mpbird ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to 2\mathrm{MonoAP}{F}$
96 39 95 sylanl2 ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge \left({F}\left({x}\right)={F}\left({y}\right)\wedge {x}<{y}\right)\right)\to 2\mathrm{MonoAP}{F}$
97 96 expr ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to \left({x}<{y}\to 2\mathrm{MonoAP}{F}\right)$
98 38 97 mtod ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to ¬{x}<{y}$
99 simplr1 ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to {x}\in \left(1\dots \left|{R}\right|+1\right)$
100 99 33 syl ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to {x}\in ℝ$
101 simplr2 ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to {y}\in \left(1\dots \left|{R}\right|+1\right)$
102 34 101 sseldi ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to {y}\in ℝ$
103 100 102 eqleltd ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to \left({x}={y}↔\left({x}\le {y}\wedge ¬{x}<{y}\right)\right)$
104 37 98 103 mpbir2and ${⊢}\left(\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\wedge {F}\left({x}\right)={F}\left({y}\right)\right)\to {x}={y}$
105 104 ex ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\wedge {x}\le {y}\right)\right)\to \left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
106 22 31 35 36 105 wlogle ${⊢}\left({\phi }\wedge \left({x}\in \left(1\dots \left|{R}\right|+1\right)\wedge {y}\in \left(1\dots \left|{R}\right|+1\right)\right)\right)\to \left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
107 106 ralrimivva ${⊢}{\phi }\to \forall {x}\in \left(1\dots \left|{R}\right|+1\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(1\dots \left|{R}\right|+1\right)\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)$
108 dff13 ${⊢}{F}:\left(1\dots \left|{R}\right|+1\right)\underset{1-1}{⟶}{R}↔\left({F}:\left(1\dots \left|{R}\right|+1\right)⟶{R}\wedge \forall {x}\in \left(1\dots \left|{R}\right|+1\right)\phantom{\rule{.4em}{0ex}}\forall {y}\in \left(1\dots \left|{R}\right|+1\right)\phantom{\rule{.4em}{0ex}}\left({F}\left({x}\right)={F}\left({y}\right)\to {x}={y}\right)\right)$
109 2 107 108 sylanbrc ${⊢}{\phi }\to {F}:\left(1\dots \left|{R}\right|+1\right)\underset{1-1}{⟶}{R}$
110 f1domg ${⊢}{R}\in \mathrm{Fin}\to \left({F}:\left(1\dots \left|{R}\right|+1\right)\underset{1-1}{⟶}{R}\to \left(1\dots \left|{R}\right|+1\right)\preccurlyeq {R}\right)$
111 1 109 110 sylc ${⊢}{\phi }\to \left(1\dots \left|{R}\right|+1\right)\preccurlyeq {R}$
112 domnsym ${⊢}\left(1\dots \left|{R}\right|+1\right)\preccurlyeq {R}\to ¬{R}\prec \left(1\dots \left|{R}\right|+1\right)$
113 111 112 syl ${⊢}{\phi }\to ¬{R}\prec \left(1\dots \left|{R}\right|+1\right)$
114 17 113 pm2.65i ${⊢}¬{\phi }$