Theorem fi1uzind

Description: Properties of an ordered pair with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (represented as orderd pairs of vertices and edges) with a finite number of vertices, usually with L = 0 (see opfi1ind ) or L = 1 . (Contributed by AV, 22-Oct-2020) (Revised by AV, 28-Mar-2021)

	Ref	Expression
Hypotheses	fi1uzind.f	$$⊢F\in \mathrm{V}$$
	fi1uzind.l	$$⊢L\in {\mathbb{N}}_0$$
	fi1uzind.1	$$⊢\left(v=V\wedge e=E\right)\to \left(\psi \leftrightarrow \phi \right)$$
	fi1uzind.2	$$⊢\left(v=w\wedge e=f\right)\to \left(\psi \leftrightarrow \theta \right)$$
	fi1uzind.3	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n\in v\right)\to \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho$$
	fi1uzind.4	$$⊢\left(w=v\setminus \left\{n\right\}\wedge f=F\right)\to \left(\theta \leftrightarrow \chi \right)$$
	fi1uzind.base	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge \left|v\right|=L\right)\to \psi$$
	fi1uzind.step	$$⊢\left(\left(y+1\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge \left|v\right|=y+1\wedge n\in v\right)\right)\wedge \chi \right)\to \psi$$
Assertion	fi1uzind	$$⊢\left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \wedge V\in \mathrm{Fin}\wedge L\le \left|V\right|\right)\to \phi$$

Proof

Step	Hyp	Ref	Expression
1		fi1uzind.f	$$⊢F\in \mathrm{V}$$
2		fi1uzind.l	$$⊢L\in {\mathbb{N}}_0$$
3		fi1uzind.1	$$⊢\left(v=V\wedge e=E\right)\to \left(\psi \leftrightarrow \phi \right)$$
4		fi1uzind.2	$$⊢\left(v=w\wedge e=f\right)\to \left(\psi \leftrightarrow \theta \right)$$
5		fi1uzind.3	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n\in v\right)\to \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho$$
6		fi1uzind.4	$$⊢\left(w=v\setminus \left\{n\right\}\wedge f=F\right)\to \left(\theta \leftrightarrow \chi \right)$$
7		fi1uzind.base	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge \left|v\right|=L\right)\to \psi$$
8		fi1uzind.step	$$⊢\left(\left(y+1\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge \left|v\right|=y+1\wedge n\in v\right)\right)\wedge \chi \right)\to \psi$$
9		dfclel	$$⊢\left|V\right|\in {\mathbb{N}}_0\leftrightarrow \exists n\left(n=\left|V\right|\wedge n\in {\mathbb{N}}_0\right)$$
10		nn0z	$$⊢L\in {\mathbb{N}}_0\to L\in \mathbb{Z}$$
11	2 10	mp1i	$$⊢\left(\left(L\le \left|V\right|\wedge n\in {\mathbb{N}}_0\right)\wedge n=\left|V\right|\right)\to L\in \mathbb{Z}$$
12		nn0z	$$⊢n\in {\mathbb{N}}_0\to n\in \mathbb{Z}$$
13	12	ad2antlr	$$⊢\left(\left(L\le \left|V\right|\wedge n\in {\mathbb{N}}_0\right)\wedge n=\left|V\right|\right)\to n\in \mathbb{Z}$$
14		breq2	$$⊢\left|V\right|=n\to \left(L\le \left|V\right|\leftrightarrow L\le n\right)$$
15	14	eqcoms	$$⊢n=\left|V\right|\to \left(L\le \left|V\right|\leftrightarrow L\le n\right)$$
16	15	biimpcd	$$⊢L\le \left|V\right|\to \left(n=\left|V\right|\to L\le n\right)$$
17	16	adantr	$$⊢\left(L\le \left|V\right|\wedge n\in {\mathbb{N}}_0\right)\to \left(n=\left|V\right|\to L\le n\right)$$
18	17	imp	$$⊢\left(\left(L\le \left|V\right|\wedge n\in {\mathbb{N}}_0\right)\wedge n=\left|V\right|\right)\to L\le n$$
19		eqeq1	$$⊢x=L\to \left(x=\left|v\right|\leftrightarrow L=\left|v\right|\right)$$
20	19	anbi2d	$$⊢x=L\to \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\leftrightarrow \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge L=\left|v\right|\right)\right)$$
21	20	imbi1d	$$⊢x=L\to \left(\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\to \psi \right)\leftrightarrow \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge L=\left|v\right|\right)\to \psi \right)\right)$$
22	21	2albidv	$$⊢x=L\to \left(\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\to \psi \right)\leftrightarrow \forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge L=\left|v\right|\right)\to \psi \right)\right)$$
23		eqeq1	$$⊢x=y\to \left(x=\left|v\right|\leftrightarrow y=\left|v\right|\right)$$
24	23	anbi2d	$$⊢x=y\to \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\leftrightarrow \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y=\left|v\right|\right)\right)$$
25	24	imbi1d	$$⊢x=y\to \left(\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\to \psi \right)\leftrightarrow \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y=\left|v\right|\right)\to \psi \right)\right)$$
26	25	2albidv	$$⊢x=y\to \left(\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\to \psi \right)\leftrightarrow \forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y=\left|v\right|\right)\to \psi \right)\right)$$
27		eqeq1	$$⊢x=y+1\to \left(x=\left|v\right|\leftrightarrow y+1=\left|v\right|\right)$$
28	27	anbi2d	$$⊢x=y+1\to \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\leftrightarrow \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\right)$$
29	28	imbi1d	$$⊢x=y+1\to \left(\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\to \psi \right)\leftrightarrow \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\to \psi \right)\right)$$
30	29	2albidv	$$⊢x=y+1\to \left(\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\to \psi \right)\leftrightarrow \forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\to \psi \right)\right)$$
31		eqeq1	$$⊢x=n\to \left(x=\left|v\right|\leftrightarrow n=\left|v\right|\right)$$
32	31	anbi2d	$$⊢x=n\to \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\leftrightarrow \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\right)$$
33	32	imbi1d	$$⊢x=n\to \left(\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\to \psi \right)\leftrightarrow \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\to \psi \right)\right)$$
34	33	2albidv	$$⊢x=n\to \left(\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge x=\left|v\right|\right)\to \psi \right)\leftrightarrow \forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\to \psi \right)\right)$$
35		eqcom	$$⊢L=\left|v\right|\leftrightarrow \left|v\right|=L$$
36	35 7	sylan2b	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge L=\left|v\right|\right)\to \psi$$
37	36	gen2	$$⊢\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge L=\left|v\right|\right)\to \psi \right)$$
38	37	a1i	$$⊢L\in \mathbb{Z}\to \forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge L=\left|v\right|\right)\to \psi \right)$$
39		simpl	$$⊢\left(v=w\wedge e=f\right)\to v=w$$
40		simpr	$$⊢\left(v=w\wedge e=f\right)\to e=f$$
41	40	sbceq1d	$$⊢\left(v=w\wedge e=f\right)\to \left(\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \leftrightarrow \underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \right)$$
42	39 41	sbceqbid	$$⊢\left(v=w\wedge e=f\right)\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \leftrightarrow \underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \right)$$
43		fveq2	$$⊢v=w\to \left|v\right|=\left|w\right|$$
44	43	eqeq2d	$$⊢v=w\to \left(y=\left|v\right|\leftrightarrow y=\left|w\right|\right)$$
45	44	adantr	$$⊢\left(v=w\wedge e=f\right)\to \left(y=\left|v\right|\leftrightarrow y=\left|w\right|\right)$$
46	42 45	anbi12d	$$⊢\left(v=w\wedge e=f\right)\to \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y=\left|v\right|\right)\leftrightarrow \left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\right)$$
47	46 4	imbi12d	$$⊢\left(v=w\wedge e=f\right)\to \left(\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y=\left|v\right|\right)\to \psi \right)\leftrightarrow \left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\right)$$
48	47	cbval2vw	$$⊢\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y=\left|v\right|\right)\to \psi \right)\leftrightarrow \forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)$$
49		nn0ge0	$$⊢L\in {\mathbb{N}}_0\to 0\le L$$
50		0red	$$⊢y\in \mathbb{Z}\to 0\in ℝ$$
51		nn0re	$$⊢L\in {\mathbb{N}}_0\to L\in ℝ$$
52	2 51	mp1i	$$⊢y\in \mathbb{Z}\to L\in ℝ$$
53		zre	$$⊢y\in \mathbb{Z}\to y\in ℝ$$
54		letr	$$⊢\left(0\in ℝ\wedge L\in ℝ\wedge y\in ℝ\right)\to \left(\left(0\le L\wedge L\le y\right)\to 0\le y\right)$$
55	50 52 53 54	syl3anc	$$⊢y\in \mathbb{Z}\to \left(\left(0\le L\wedge L\le y\right)\to 0\le y\right)$$
56		0nn0	$$⊢0\in {\mathbb{N}}_0$$
57		pm3.22	$$⊢\left(0\le y\wedge y\in \mathbb{Z}\right)\to \left(y\in \mathbb{Z}\wedge 0\le y\right)$$
58		0z	$$⊢0\in \mathbb{Z}$$
59		eluz1	$$⊢0\in \mathbb{Z}\to \left(y\in {\mathbb{Z}}_{\ge 0}\leftrightarrow \left(y\in \mathbb{Z}\wedge 0\le y\right)\right)$$
60	58 59	mp1i	$$⊢\left(0\le y\wedge y\in \mathbb{Z}\right)\to \left(y\in {\mathbb{Z}}_{\ge 0}\leftrightarrow \left(y\in \mathbb{Z}\wedge 0\le y\right)\right)$$
61	57 60	mpbird	$$⊢\left(0\le y\wedge y\in \mathbb{Z}\right)\to y\in {\mathbb{Z}}_{\ge 0}$$
62		eluznn0	$$⊢\left(0\in {\mathbb{N}}_0\wedge y\in {\mathbb{Z}}_{\ge 0}\right)\to y\in {\mathbb{N}}_0$$
63	56 61 62	sylancr	$$⊢\left(0\le y\wedge y\in \mathbb{Z}\right)\to y\in {\mathbb{N}}_0$$
64	63	ex	$$⊢0\le y\to \left(y\in \mathbb{Z}\to y\in {\mathbb{N}}_0\right)$$
65	55 64	syl6com	$$⊢\left(0\le L\wedge L\le y\right)\to \left(y\in \mathbb{Z}\to \left(y\in \mathbb{Z}\to y\in {\mathbb{N}}_0\right)\right)$$
66	65	ex	$$⊢0\le L\to \left(L\le y\to \left(y\in \mathbb{Z}\to \left(y\in \mathbb{Z}\to y\in {\mathbb{N}}_0\right)\right)\right)$$
67	66	com14	$$⊢y\in \mathbb{Z}\to \left(L\le y\to \left(y\in \mathbb{Z}\to \left(0\le L\to y\in {\mathbb{N}}_0\right)\right)\right)$$
68	67	pm2.43a	$$⊢y\in \mathbb{Z}\to \left(L\le y\to \left(0\le L\to y\in {\mathbb{N}}_0\right)\right)$$
69	68	imp	$$⊢\left(y\in \mathbb{Z}\wedge L\le y\right)\to \left(0\le L\to y\in {\mathbb{N}}_0\right)$$
70	69	com12	$$⊢0\le L\to \left(\left(y\in \mathbb{Z}\wedge L\le y\right)\to y\in {\mathbb{N}}_0\right)$$
71	2 49 70	mp2b	$$⊢\left(y\in \mathbb{Z}\wedge L\le y\right)\to y\in {\mathbb{N}}_0$$
72	71	3adant1	$$⊢\left(L\in \mathbb{Z}\wedge y\in \mathbb{Z}\wedge L\le y\right)\to y\in {\mathbb{N}}_0$$
73		eqcom	$$⊢y+1=\left|v\right|\leftrightarrow \left|v\right|=y+1$$
74		nn0p1gt0	$$⊢y\in {\mathbb{N}}_0\to 0<y+1$$
75	74	adantr	$$⊢\left(y\in {\mathbb{N}}_0\wedge \left|v\right|=y+1\right)\to 0<y+1$$
76		simpr	$$⊢\left(y\in {\mathbb{N}}_0\wedge \left|v\right|=y+1\right)\to \left|v\right|=y+1$$
77	75 76	breqtrrd	$$⊢\left(y\in {\mathbb{N}}_0\wedge \left|v\right|=y+1\right)\to 0<\left|v\right|$$
78	73 77	sylan2b	$$⊢\left(y\in {\mathbb{N}}_0\wedge y+1=\left|v\right|\right)\to 0<\left|v\right|$$
79	78	adantrl	$$⊢\left(y\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\right)\to 0<\left|v\right|$$
80		hashgt0elex	$$⊢\left(v\in \mathrm{V}\wedge 0<\left|v\right|\right)\to \exists nn\in v$$
81		vex	$$⊢v\in \mathrm{V}$$
82	81	a1i	$$⊢\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\to v\in \mathrm{V}$$
83		simpr	$$⊢\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\to n\in v$$
84		simpl	$$⊢\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\to y\in {\mathbb{N}}_0$$
85		hashdifsnp1	$$⊢\left(v\in \mathrm{V}\wedge n\in v\wedge y\in {\mathbb{N}}_0\right)\to \left(\left|v\right|=y+1\to \left|v\setminus \left\{n\right\}\right|=y\right)$$
86	73 85	syl5bi	$$⊢\left(v\in \mathrm{V}\wedge n\in v\wedge y\in {\mathbb{N}}_0\right)\to \left(y+1=\left|v\right|\to \left|v\setminus \left\{n\right\}\right|=y\right)$$
87	82 83 84 86	syl3anc	$$⊢\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\to \left(y+1=\left|v\right|\to \left|v\setminus \left\{n\right\}\right|=y\right)$$
88	87	imp	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\to \left|v\setminus \left\{n\right\}\right|=y$$
89		peano2nn0	$$⊢y\in {\mathbb{N}}_0\to y+1\in {\mathbb{N}}_0$$
90	89	ad2antrr	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\to y+1\in {\mathbb{N}}_0$$
91	90	ad2antlr	$$⊢\left(\left(\left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\wedge \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)\wedge \left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\right)\wedge \underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \right)\to y+1\in {\mathbb{N}}_0$$
92		simpr	$$⊢\left(\left(\left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\wedge \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)\wedge \left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\right)\wedge \underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \right)\to \underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho$$
93		simplrr	$$⊢\left(\left(\left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\wedge \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)\wedge \left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\right)\wedge \underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \right)\to y+1=\left|v\right|$$
94		simprlr	$$⊢\left(\left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\wedge \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)\wedge \left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\right)\to n\in v$$
95	94	adantr	$$⊢\left(\left(\left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\wedge \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)\wedge \left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\right)\wedge \underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \right)\to n\in v$$
96	92 93 95	3jca	$$⊢\left(\left(\left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\wedge \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)\wedge \left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\right)\wedge \underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \right)\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\wedge n\in v\right)$$
97	91 96	jca	$$⊢\left(\left(\left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\wedge \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)\wedge \left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\right)\wedge \underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \right)\to \left(y+1\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\wedge n\in v\right)\right)$$
98	81	difexi	$$⊢v\setminus \left\{n\right\}\in \mathrm{V}$$
99		simpl	$$⊢\left(w=v\setminus \left\{n\right\}\wedge f=F\right)\to w=v\setminus \left\{n\right\}$$
100		simpr	$$⊢\left(w=v\setminus \left\{n\right\}\wedge f=F\right)\to f=F$$
101	100	sbceq1d	$$⊢\left(w=v\setminus \left\{n\right\}\wedge f=F\right)\to \left(\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \leftrightarrow \underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)$$
102	99 101	sbceqbid	$$⊢\left(w=v\setminus \left\{n\right\}\wedge f=F\right)\to \left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \leftrightarrow \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)$$
103		eqcom	$$⊢y=\left|w\right|\leftrightarrow \left|w\right|=y$$
104		fveqeq2	$$⊢w=v\setminus \left\{n\right\}\to \left(\left|w\right|=y\leftrightarrow \left|v\setminus \left\{n\right\}\right|=y\right)$$
105	103 104	syl5bb	$$⊢w=v\setminus \left\{n\right\}\to \left(y=\left|w\right|\leftrightarrow \left|v\setminus \left\{n\right\}\right|=y\right)$$
106	105	adantr	$$⊢\left(w=v\setminus \left\{n\right\}\wedge f=F\right)\to \left(y=\left|w\right|\leftrightarrow \left|v\setminus \left\{n\right\}\right|=y\right)$$
107	102 106	anbi12d	$$⊢\left(w=v\setminus \left\{n\right\}\wedge f=F\right)\to \left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\leftrightarrow \left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \wedge \left|v\setminus \left\{n\right\}\right|=y\right)\right)$$
108	107 6	imbi12d	$$⊢\left(w=v\setminus \left\{n\right\}\wedge f=F\right)\to \left(\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\leftrightarrow \left(\left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \wedge \left|v\setminus \left\{n\right\}\right|=y\right)\to \chi \right)\right)$$
109	108	spc2gv	$$⊢\left(v\setminus \left\{n\right\}\in \mathrm{V}\wedge F\in \mathrm{V}\right)\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \left(\left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \wedge \left|v\setminus \left\{n\right\}\right|=y\right)\to \chi \right)\right)$$
110	98 1 109	mp2an	$$⊢\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \left(\left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \wedge \left|v\setminus \left\{n\right\}\right|=y\right)\to \chi \right)$$
111	110	expdimp	$$⊢\left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\wedge \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)\to \left(\left|v\setminus \left\{n\right\}\right|=y\to \chi \right)$$
112	111	ad2antrr	$$⊢\left(\left(\left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\wedge \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)\wedge \left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\right)\wedge \underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \right)\to \left(\left|v\setminus \left\{n\right\}\right|=y\to \chi \right)$$
113	73	3anbi2i	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\wedge n\in v\right)\leftrightarrow \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge \left|v\right|=y+1\wedge n\in v\right)$$
114	113	anbi2i	$$⊢\left(y+1\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\wedge n\in v\right)\right)\leftrightarrow \left(y+1\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge \left|v\right|=y+1\wedge n\in v\right)\right)$$
115	114 8	sylanb	$$⊢\left(\left(y+1\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\wedge n\in v\right)\right)\wedge \chi \right)\to \psi$$
116	97 112 115	syl6an	$$⊢\left(\left(\left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\wedge \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \right)\wedge \left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\right)\wedge \underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \right)\to \left(\left|v\setminus \left\{n\right\}\right|=y\to \psi \right)$$
117	116	exp41	$$⊢\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \to \left(\left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\left|v\setminus \left\{n\right\}\right|=y\to \psi \right)\right)\right)\right)$$
118	117	com15	$$⊢\left|v\setminus \left\{n\right\}\right|=y\to \left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \to \left(\left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)$$
119	118	com23	$$⊢\left|v\setminus \left\{n\right\}\right|=y\to \left(\left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\to \left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)$$
120	88 119	mpcom	$$⊢\left(\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\wedge y+1=\left|v\right|\right)\to \left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)$$
121	120	ex	$$⊢\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\to \left(y+1=\left|v\right|\to \left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)$$
122	121	com23	$$⊢\left(y\in {\mathbb{N}}_0\wedge n\in v\right)\to \left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \to \left(y+1=\left|v\right|\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)$$
123	122	ex	$$⊢y\in {\mathbb{N}}_0\to \left(n\in v\to \left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \to \left(y+1=\left|v\right|\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)\right)$$
124	123	com15	$$⊢\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(n\in v\to \left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \to \left(y+1=\left|v\right|\to \left(y\in {\mathbb{N}}_0\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)\right)$$
125	124	imp	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n\in v\right)\to \left(\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}\rho \to \left(y+1=\left|v\right|\to \left(y\in {\mathbb{N}}_0\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)$$
126	5 125	mpd	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n\in v\right)\to \left(y+1=\left|v\right|\to \left(y\in {\mathbb{N}}_0\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)$$
127	126	ex	$$⊢\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(n\in v\to \left(y+1=\left|v\right|\to \left(y\in {\mathbb{N}}_0\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)$$
128	127	com4l	$$⊢n\in v\to \left(y+1=\left|v\right|\to \left(y\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)$$
129	128	exlimiv	$$⊢\exists nn\in v\to \left(y+1=\left|v\right|\to \left(y\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)$$
130	80 129	syl	$$⊢\left(v\in \mathrm{V}\wedge 0<\left|v\right|\right)\to \left(y+1=\left|v\right|\to \left(y\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)$$
131	130	ex	$$⊢v\in \mathrm{V}\to \left(0<\left|v\right|\to \left(y+1=\left|v\right|\to \left(y\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)\right)$$
132	131	com25	$$⊢v\in \mathrm{V}\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(y+1=\left|v\right|\to \left(y\in {\mathbb{N}}_0\to \left(0<\left|v\right|\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)\right)$$
133	132	elv	$$⊢\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \to \left(y+1=\left|v\right|\to \left(y\in {\mathbb{N}}_0\to \left(0<\left|v\right|\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)\right)$$
134	133	imp	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\to \left(y\in {\mathbb{N}}_0\to \left(0<\left|v\right|\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)\right)$$
135	134	impcom	$$⊢\left(y\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\right)\to \left(0<\left|v\right|\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)\right)$$
136	79 135	mpd	$$⊢\left(y\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\right)\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)$$
137	72 136	sylan	$$⊢\left(\left(L\in \mathbb{Z}\wedge y\in \mathbb{Z}\wedge L\le y\right)\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\right)\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \psi \right)$$
138	137	impancom	$$⊢\left(\left(L\in \mathbb{Z}\wedge y\in \mathbb{Z}\wedge L\le y\right)\wedge \forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\right)\to \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\to \psi \right)$$
139	138	alrimivv	$$⊢\left(\left(L\in \mathbb{Z}\wedge y\in \mathbb{Z}\wedge L\le y\right)\wedge \forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\right)\to \forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\to \psi \right)$$
140	139	ex	$$⊢\left(L\in \mathbb{Z}\wedge y\in \mathbb{Z}\wedge L\le y\right)\to \left(\forall w\forall f\left(\left(\underset{\dot{}}{[}w/a\underset{\dot{}}{]}\underset{\dot{}}{[}f/b\underset{\dot{}}{]}\rho \wedge y=\left|w\right|\right)\to \theta \right)\to \forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\to \psi \right)\right)$$
141	48 140	syl5bi	$$⊢\left(L\in \mathbb{Z}\wedge y\in \mathbb{Z}\wedge L\le y\right)\to \left(\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y=\left|v\right|\right)\to \psi \right)\to \forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge y+1=\left|v\right|\right)\to \psi \right)\right)$$
142	22 26 30 34 38 141	uzind	$$⊢\left(L\in \mathbb{Z}\wedge n\in \mathbb{Z}\wedge L\le n\right)\to \forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\to \psi \right)$$
143	11 13 18 142	syl3anc	$$⊢\left(\left(L\le \left|V\right|\wedge n\in {\mathbb{N}}_0\right)\wedge n=\left|V\right|\right)\to \forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\to \psi \right)$$
144		sbcex	$$⊢\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to V\in \mathrm{V}$$
145		sbccom	$$⊢\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \leftrightarrow \underset{\dot{}}{[}E/b\underset{\dot{}}{]}\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\rho$$
146		sbcex	$$⊢\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\rho \to E\in \mathrm{V}$$
147	145 146	sylbi	$$⊢\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to E\in \mathrm{V}$$
148	144 147	jca	$$⊢\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to \left(V\in \mathrm{V}\wedge E\in \mathrm{V}\right)$$
149		simpl	$$⊢\left(v=V\wedge e=E\right)\to v=V$$
150		simpr	$$⊢\left(v=V\wedge e=E\right)\to e=E$$
151	150	sbceq1d	$$⊢\left(v=V\wedge e=E\right)\to \left(\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \leftrightarrow \underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \right)$$
152	149 151	sbceqbid	$$⊢\left(v=V\wedge e=E\right)\to \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \leftrightarrow \underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \right)$$
153		fveq2	$$⊢v=V\to \left|v\right|=\left|V\right|$$
154	153	eqeq2d	$$⊢v=V\to \left(n=\left|v\right|\leftrightarrow n=\left|V\right|\right)$$
155	154	adantr	$$⊢\left(v=V\wedge e=E\right)\to \left(n=\left|v\right|\leftrightarrow n=\left|V\right|\right)$$
156	152 155	anbi12d	$$⊢\left(v=V\wedge e=E\right)\to \left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\leftrightarrow \left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \wedge n=\left|V\right|\right)\right)$$
157	156 3	imbi12d	$$⊢\left(v=V\wedge e=E\right)\to \left(\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\to \psi \right)\leftrightarrow \left(\left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \wedge n=\left|V\right|\right)\to \phi \right)\right)$$
158	157	spc2gv	$$⊢\left(V\in \mathrm{V}\wedge E\in \mathrm{V}\right)\to \left(\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\to \psi \right)\to \left(\left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \wedge n=\left|V\right|\right)\to \phi \right)\right)$$
159	158	com23	$$⊢\left(V\in \mathrm{V}\wedge E\in \mathrm{V}\right)\to \left(\left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \wedge n=\left|V\right|\right)\to \left(\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\to \psi \right)\to \phi \right)\right)$$
160	159	expd	$$⊢\left(V\in \mathrm{V}\wedge E\in \mathrm{V}\right)\to \left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to \left(n=\left|V\right|\to \left(\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\to \psi \right)\to \phi \right)\right)\right)$$
161	148 160	mpcom	$$⊢\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to \left(n=\left|V\right|\to \left(\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\to \psi \right)\to \phi \right)\right)$$
162	161	imp	$$⊢\left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \wedge n=\left|V\right|\right)\to \left(\forall v\forall e\left(\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}\rho \wedge n=\left|v\right|\right)\to \psi \right)\to \phi \right)$$
163	143 162	syl5com	$$⊢\left(\left(L\le \left|V\right|\wedge n\in {\mathbb{N}}_0\right)\wedge n=\left|V\right|\right)\to \left(\left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \wedge n=\left|V\right|\right)\to \phi \right)$$
164	163	exp31	$$⊢L\le \left|V\right|\to \left(n\in {\mathbb{N}}_0\to \left(n=\left|V\right|\to \left(\left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \wedge n=\left|V\right|\right)\to \phi \right)\right)\right)$$
165	164	com14	$$⊢\left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \wedge n=\left|V\right|\right)\to \left(n\in {\mathbb{N}}_0\to \left(n=\left|V\right|\to \left(L\le \left|V\right|\to \phi \right)\right)\right)$$
166	165	expcom	$$⊢n=\left|V\right|\to \left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to \left(n\in {\mathbb{N}}_0\to \left(n=\left|V\right|\to \left(L\le \left|V\right|\to \phi \right)\right)\right)\right)$$
167	166	com24	$$⊢n=\left|V\right|\to \left(n=\left|V\right|\to \left(n\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to \left(L\le \left|V\right|\to \phi \right)\right)\right)\right)$$
168	167	pm2.43i	$$⊢n=\left|V\right|\to \left(n\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to \left(L\le \left|V\right|\to \phi \right)\right)\right)$$
169	168	imp	$$⊢\left(n=\left|V\right|\wedge n\in {\mathbb{N}}_0\right)\to \left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to \left(L\le \left|V\right|\to \phi \right)\right)$$
170	169	exlimiv	$$⊢\exists n\left(n=\left|V\right|\wedge n\in {\mathbb{N}}_0\right)\to \left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to \left(L\le \left|V\right|\to \phi \right)\right)$$
171	9 170	sylbi	$$⊢\left|V\right|\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to \left(L\le \left|V\right|\to \phi \right)\right)$$
172		hashcl	$$⊢V\in \mathrm{Fin}\to \left|V\right|\in {\mathbb{N}}_0$$
173	171 172	syl11	$$⊢\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \to \left(V\in \mathrm{Fin}\to \left(L\le \left|V\right|\to \phi \right)\right)$$
174	173	3imp	$$⊢\left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}\rho \wedge V\in \mathrm{Fin}\wedge L\le \left|V\right|\right)\to \phi$$