Metamath Proof Explorer

Theorem brfi1indALT

Description: Alternate proof of brfi1ind , which does not use brfi1uzind . (Contributed by Alexander van der Vekens, 7-Jan-2018) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses brfi1ind.r ${⊢}\mathrm{Rel}{G}$
brfi1ind.f ${⊢}{F}\in \mathrm{V}$
brfi1ind.1 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({\psi }↔{\phi }\right)$
brfi1ind.2 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({\psi }↔{\theta }\right)$
brfi1ind.3 ${⊢}\left({v}{G}{e}\wedge {n}\in {v}\right)\to \left({v}\setminus \left\{{n}\right\}\right){G}{F}$
brfi1ind.4 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({\theta }↔{\chi }\right)$
brfi1ind.base ${⊢}\left({v}{G}{e}\wedge \left|{v}\right|=0\right)\to {\psi }$
brfi1ind.step ${⊢}\left(\left({y}+1\in {ℕ}_{0}\wedge \left({v}{G}{e}\wedge \left|{v}\right|={y}+1\wedge {n}\in {v}\right)\right)\wedge {\chi }\right)\to {\psi }$
Assertion brfi1indALT ${⊢}\left({V}{G}{E}\wedge {V}\in \mathrm{Fin}\right)\to {\phi }$

Proof

Step Hyp Ref Expression
1 brfi1ind.r ${⊢}\mathrm{Rel}{G}$
2 brfi1ind.f ${⊢}{F}\in \mathrm{V}$
3 brfi1ind.1 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({\psi }↔{\phi }\right)$
4 brfi1ind.2 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({\psi }↔{\theta }\right)$
5 brfi1ind.3 ${⊢}\left({v}{G}{e}\wedge {n}\in {v}\right)\to \left({v}\setminus \left\{{n}\right\}\right){G}{F}$
6 brfi1ind.4 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({\theta }↔{\chi }\right)$
7 brfi1ind.base ${⊢}\left({v}{G}{e}\wedge \left|{v}\right|=0\right)\to {\psi }$
8 brfi1ind.step ${⊢}\left(\left({y}+1\in {ℕ}_{0}\wedge \left({v}{G}{e}\wedge \left|{v}\right|={y}+1\wedge {n}\in {v}\right)\right)\wedge {\chi }\right)\to {\psi }$
9 hashcl ${⊢}{V}\in \mathrm{Fin}\to \left|{V}\right|\in {ℕ}_{0}$
10 dfclel ${⊢}\left|{V}\right|\in {ℕ}_{0}↔\exists {n}\phantom{\rule{.4em}{0ex}}\left({n}=\left|{V}\right|\wedge {n}\in {ℕ}_{0}\right)$
11 eqeq2 ${⊢}{x}=0\to \left(\left|{v}\right|={x}↔\left|{v}\right|=0\right)$
12 11 anbi2d ${⊢}{x}=0\to \left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)↔\left({v}{G}{e}\wedge \left|{v}\right|=0\right)\right)$
13 12 imbi1d ${⊢}{x}=0\to \left(\left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)\to {\psi }\right)↔\left(\left({v}{G}{e}\wedge \left|{v}\right|=0\right)\to {\psi }\right)\right)$
14 13 2albidv ${⊢}{x}=0\to \left(\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)\to {\psi }\right)↔\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|=0\right)\to {\psi }\right)\right)$
15 eqeq2 ${⊢}{x}={y}\to \left(\left|{v}\right|={x}↔\left|{v}\right|={y}\right)$
16 15 anbi2d ${⊢}{x}={y}\to \left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)↔\left({v}{G}{e}\wedge \left|{v}\right|={y}\right)\right)$
17 16 imbi1d ${⊢}{x}={y}\to \left(\left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)\to {\psi }\right)↔\left(\left({v}{G}{e}\wedge \left|{v}\right|={y}\right)\to {\psi }\right)\right)$
18 17 2albidv ${⊢}{x}={y}\to \left(\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)\to {\psi }\right)↔\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={y}\right)\to {\psi }\right)\right)$
19 eqeq2 ${⊢}{x}={y}+1\to \left(\left|{v}\right|={x}↔\left|{v}\right|={y}+1\right)$
20 19 anbi2d ${⊢}{x}={y}+1\to \left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)↔\left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\right)$
21 20 imbi1d ${⊢}{x}={y}+1\to \left(\left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)\to {\psi }\right)↔\left(\left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\to {\psi }\right)\right)$
22 21 2albidv ${⊢}{x}={y}+1\to \left(\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)\to {\psi }\right)↔\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\to {\psi }\right)\right)$
23 eqeq2 ${⊢}{x}={n}\to \left(\left|{v}\right|={x}↔\left|{v}\right|={n}\right)$
24 23 anbi2d ${⊢}{x}={n}\to \left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)↔\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)\right)$
25 24 imbi1d ${⊢}{x}={n}\to \left(\left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)\to {\psi }\right)↔\left(\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)\to {\psi }\right)\right)$
26 25 2albidv ${⊢}{x}={n}\to \left(\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={x}\right)\to {\psi }\right)↔\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)\to {\psi }\right)\right)$
27 7 gen2 ${⊢}\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|=0\right)\to {\psi }\right)$
28 breq12 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({v}{G}{e}↔{w}{G}{f}\right)$
29 fveq2 ${⊢}{v}={w}\to \left|{v}\right|=\left|{w}\right|$
30 29 eqeq1d ${⊢}{v}={w}\to \left(\left|{v}\right|={y}↔\left|{w}\right|={y}\right)$
31 30 adantr ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left(\left|{v}\right|={y}↔\left|{w}\right|={y}\right)$
32 28 31 anbi12d ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left(\left({v}{G}{e}\wedge \left|{v}\right|={y}\right)↔\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\right)$
33 32 4 imbi12d ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left(\left(\left({v}{G}{e}\wedge \left|{v}\right|={y}\right)\to {\psi }\right)↔\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\right)$
34 33 cbval2vv ${⊢}\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={y}\right)\to {\psi }\right)↔\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)$
35 nn0re ${⊢}{y}\in {ℕ}_{0}\to {y}\in ℝ$
36 1re ${⊢}1\in ℝ$
37 36 a1i ${⊢}{y}\in {ℕ}_{0}\to 1\in ℝ$
38 nn0ge0 ${⊢}{y}\in {ℕ}_{0}\to 0\le {y}$
39 0lt1 ${⊢}0<1$
40 39 a1i ${⊢}{y}\in {ℕ}_{0}\to 0<1$
41 35 37 38 40 addgegt0d ${⊢}{y}\in {ℕ}_{0}\to 0<{y}+1$
42 41 adantr ${⊢}\left({y}\in {ℕ}_{0}\wedge \left|{v}\right|={y}+1\right)\to 0<{y}+1$
43 simpr ${⊢}\left({y}\in {ℕ}_{0}\wedge \left|{v}\right|={y}+1\right)\to \left|{v}\right|={y}+1$
44 42 43 breqtrrd ${⊢}\left({y}\in {ℕ}_{0}\wedge \left|{v}\right|={y}+1\right)\to 0<\left|{v}\right|$
45 44 adantrl ${⊢}\left({y}\in {ℕ}_{0}\wedge \left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\right)\to 0<\left|{v}\right|$
46 vex ${⊢}{v}\in \mathrm{V}$
47 hashgt0elex ${⊢}\left({v}\in \mathrm{V}\wedge 0<\left|{v}\right|\right)\to \exists {n}\phantom{\rule{.4em}{0ex}}{n}\in {v}$
48 46 a1i ${⊢}\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\to {v}\in \mathrm{V}$
49 simpr ${⊢}\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\to {n}\in {v}$
50 simpl ${⊢}\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\to {y}\in {ℕ}_{0}$
51 hashdifsnp1 ${⊢}\left({v}\in \mathrm{V}\wedge {n}\in {v}\wedge {y}\in {ℕ}_{0}\right)\to \left(\left|{v}\right|={y}+1\to \left|{v}\setminus \left\{{n}\right\}\right|={y}\right)$
52 48 49 50 51 syl3anc ${⊢}\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\to \left(\left|{v}\right|={y}+1\to \left|{v}\setminus \left\{{n}\right\}\right|={y}\right)$
53 52 imp ${⊢}\left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\to \left|{v}\setminus \left\{{n}\right\}\right|={y}$
54 peano2nn0 ${⊢}{y}\in {ℕ}_{0}\to {y}+1\in {ℕ}_{0}$
55 54 ad2antrr ${⊢}\left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\to {y}+1\in {ℕ}_{0}$
56 55 ad2antlr ${⊢}\left(\left(\left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\wedge \left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)\wedge \left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\right)\wedge {v}{G}{e}\right)\to {y}+1\in {ℕ}_{0}$
57 simpr ${⊢}\left(\left(\left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\wedge \left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)\wedge \left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\right)\wedge {v}{G}{e}\right)\to {v}{G}{e}$
58 simplrr ${⊢}\left(\left(\left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\wedge \left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)\wedge \left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\right)\wedge {v}{G}{e}\right)\to \left|{v}\right|={y}+1$
59 simprlr ${⊢}\left(\left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\wedge \left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)\wedge \left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\right)\to {n}\in {v}$
60 59 adantr ${⊢}\left(\left(\left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\wedge \left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)\wedge \left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\right)\wedge {v}{G}{e}\right)\to {n}\in {v}$
61 57 58 60 3jca ${⊢}\left(\left(\left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\wedge \left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)\wedge \left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\right)\wedge {v}{G}{e}\right)\to \left({v}{G}{e}\wedge \left|{v}\right|={y}+1\wedge {n}\in {v}\right)$
62 56 61 jca ${⊢}\left(\left(\left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\wedge \left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)\wedge \left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\right)\wedge {v}{G}{e}\right)\to \left({y}+1\in {ℕ}_{0}\wedge \left({v}{G}{e}\wedge \left|{v}\right|={y}+1\wedge {n}\in {v}\right)\right)$
63 difexg ${⊢}{v}\in \mathrm{V}\to {v}\setminus \left\{{n}\right\}\in \mathrm{V}$
64 46 63 ax-mp ${⊢}{v}\setminus \left\{{n}\right\}\in \mathrm{V}$
65 breq12 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({w}{G}{f}↔\left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)$
66 fveq2 ${⊢}{w}={v}\setminus \left\{{n}\right\}\to \left|{w}\right|=\left|{v}\setminus \left\{{n}\right\}\right|$
67 66 eqeq1d ${⊢}{w}={v}\setminus \left\{{n}\right\}\to \left(\left|{w}\right|={y}↔\left|{v}\setminus \left\{{n}\right\}\right|={y}\right)$
68 67 adantr ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left(\left|{w}\right|={y}↔\left|{v}\setminus \left\{{n}\right\}\right|={y}\right)$
69 65 68 anbi12d ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)↔\left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\wedge \left|{v}\setminus \left\{{n}\right\}\right|={y}\right)\right)$
70 69 6 imbi12d ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left(\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)↔\left(\left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\wedge \left|{v}\setminus \left\{{n}\right\}\right|={y}\right)\to {\chi }\right)\right)$
71 70 spc2gv ${⊢}\left({v}\setminus \left\{{n}\right\}\in \mathrm{V}\wedge {F}\in \mathrm{V}\right)\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to \left(\left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\wedge \left|{v}\setminus \left\{{n}\right\}\right|={y}\right)\to {\chi }\right)\right)$
72 64 2 71 mp2an ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to \left(\left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\wedge \left|{v}\setminus \left\{{n}\right\}\right|={y}\right)\to {\chi }\right)$
73 72 expdimp ${⊢}\left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\wedge \left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)\to \left(\left|{v}\setminus \left\{{n}\right\}\right|={y}\to {\chi }\right)$
74 73 ad2antrr ${⊢}\left(\left(\left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\wedge \left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)\wedge \left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\right)\wedge {v}{G}{e}\right)\to \left(\left|{v}\setminus \left\{{n}\right\}\right|={y}\to {\chi }\right)$
75 62 74 8 syl6an ${⊢}\left(\left(\left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\wedge \left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)\wedge \left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\right)\wedge {v}{G}{e}\right)\to \left(\left|{v}\setminus \left\{{n}\right\}\right|={y}\to {\psi }\right)$
76 75 exp41 ${⊢}\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to \left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\to \left(\left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\to \left({v}{G}{e}\to \left(\left|{v}\setminus \left\{{n}\right\}\right|={y}\to {\psi }\right)\right)\right)\right)$
77 76 com15 ${⊢}\left|{v}\setminus \left\{{n}\right\}\right|={y}\to \left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\to \left(\left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\to \left({v}{G}{e}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)$
78 77 com23 ${⊢}\left|{v}\setminus \left\{{n}\right\}\right|={y}\to \left(\left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\to \left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\to \left({v}{G}{e}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)$
79 53 78 mpcom ${⊢}\left(\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\wedge \left|{v}\right|={y}+1\right)\to \left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\to \left({v}{G}{e}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)$
80 79 ex ${⊢}\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\to \left(\left|{v}\right|={y}+1\to \left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\to \left({v}{G}{e}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)$
81 80 com23 ${⊢}\left({y}\in {ℕ}_{0}\wedge {n}\in {v}\right)\to \left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\to \left(\left|{v}\right|={y}+1\to \left({v}{G}{e}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)$
82 81 ex ${⊢}{y}\in {ℕ}_{0}\to \left({n}\in {v}\to \left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\to \left(\left|{v}\right|={y}+1\to \left({v}{G}{e}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)\right)$
83 82 com15 ${⊢}{v}{G}{e}\to \left({n}\in {v}\to \left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\to \left(\left|{v}\right|={y}+1\to \left({y}\in {ℕ}_{0}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)\right)$
84 83 imp ${⊢}\left({v}{G}{e}\wedge {n}\in {v}\right)\to \left(\left({v}\setminus \left\{{n}\right\}\right){G}{F}\to \left(\left|{v}\right|={y}+1\to \left({y}\in {ℕ}_{0}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)$
85 5 84 mpd ${⊢}\left({v}{G}{e}\wedge {n}\in {v}\right)\to \left(\left|{v}\right|={y}+1\to \left({y}\in {ℕ}_{0}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)$
86 85 ex ${⊢}{v}{G}{e}\to \left({n}\in {v}\to \left(\left|{v}\right|={y}+1\to \left({y}\in {ℕ}_{0}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)$
87 86 com4l ${⊢}{n}\in {v}\to \left(\left|{v}\right|={y}+1\to \left({y}\in {ℕ}_{0}\to \left({v}{G}{e}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)$
88 87 exlimiv ${⊢}\exists {n}\phantom{\rule{.4em}{0ex}}{n}\in {v}\to \left(\left|{v}\right|={y}+1\to \left({y}\in {ℕ}_{0}\to \left({v}{G}{e}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)$
89 47 88 syl ${⊢}\left({v}\in \mathrm{V}\wedge 0<\left|{v}\right|\right)\to \left(\left|{v}\right|={y}+1\to \left({y}\in {ℕ}_{0}\to \left({v}{G}{e}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)$
90 89 ex ${⊢}{v}\in \mathrm{V}\to \left(0<\left|{v}\right|\to \left(\left|{v}\right|={y}+1\to \left({y}\in {ℕ}_{0}\to \left({v}{G}{e}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)\right)$
91 90 com25 ${⊢}{v}\in \mathrm{V}\to \left({v}{G}{e}\to \left(\left|{v}\right|={y}+1\to \left({y}\in {ℕ}_{0}\to \left(0<\left|{v}\right|\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)\right)$
92 46 91 ax-mp ${⊢}{v}{G}{e}\to \left(\left|{v}\right|={y}+1\to \left({y}\in {ℕ}_{0}\to \left(0<\left|{v}\right|\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)\right)$
93 92 imp ${⊢}\left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\to \left({y}\in {ℕ}_{0}\to \left(0<\left|{v}\right|\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)\right)$
94 93 impcom ${⊢}\left({y}\in {ℕ}_{0}\wedge \left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\right)\to \left(0<\left|{v}\right|\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)\right)$
95 45 94 mpd ${⊢}\left({y}\in {ℕ}_{0}\wedge \left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\right)\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to {\psi }\right)$
96 95 impancom ${⊢}\left({y}\in {ℕ}_{0}\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\right)\to \left(\left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\to {\psi }\right)$
97 96 alrimivv ${⊢}\left({y}\in {ℕ}_{0}\wedge \forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\right)\to \forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\to {\psi }\right)$
98 97 ex ${⊢}{y}\in {ℕ}_{0}\to \left(\forall {w}\phantom{\rule{.4em}{0ex}}\forall {f}\phantom{\rule{.4em}{0ex}}\left(\left({w}{G}{f}\wedge \left|{w}\right|={y}\right)\to {\theta }\right)\to \forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\to {\psi }\right)\right)$
99 34 98 syl5bi ${⊢}{y}\in {ℕ}_{0}\to \left(\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={y}\right)\to {\psi }\right)\to \forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={y}+1\right)\to {\psi }\right)\right)$
100 14 18 22 26 27 99 nn0ind ${⊢}{n}\in {ℕ}_{0}\to \forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)\to {\psi }\right)$
101 1 brrelex1i ${⊢}{V}{G}{E}\to {V}\in \mathrm{V}$
102 1 brrelex2i ${⊢}{V}{G}{E}\to {E}\in \mathrm{V}$
103 101 102 jca ${⊢}{V}{G}{E}\to \left({V}\in \mathrm{V}\wedge {E}\in \mathrm{V}\right)$
104 breq12 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({v}{G}{e}↔{V}{G}{E}\right)$
105 fveq2 ${⊢}{v}={V}\to \left|{v}\right|=\left|{V}\right|$
106 105 eqeq1d ${⊢}{v}={V}\to \left(\left|{v}\right|={n}↔\left|{V}\right|={n}\right)$
107 106 adantr ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left(\left|{v}\right|={n}↔\left|{V}\right|={n}\right)$
108 104 107 anbi12d ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left(\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)↔\left({V}{G}{E}\wedge \left|{V}\right|={n}\right)\right)$
109 108 3 imbi12d ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left(\left(\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)\to {\psi }\right)↔\left(\left({V}{G}{E}\wedge \left|{V}\right|={n}\right)\to {\phi }\right)\right)$
110 109 spc2gv ${⊢}\left({V}\in \mathrm{V}\wedge {E}\in \mathrm{V}\right)\to \left(\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)\to {\psi }\right)\to \left(\left({V}{G}{E}\wedge \left|{V}\right|={n}\right)\to {\phi }\right)\right)$
111 110 com23 ${⊢}\left({V}\in \mathrm{V}\wedge {E}\in \mathrm{V}\right)\to \left(\left({V}{G}{E}\wedge \left|{V}\right|={n}\right)\to \left(\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)\to {\psi }\right)\to {\phi }\right)\right)$
112 111 expd ${⊢}\left({V}\in \mathrm{V}\wedge {E}\in \mathrm{V}\right)\to \left({V}{G}{E}\to \left(\left|{V}\right|={n}\to \left(\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)\to {\psi }\right)\to {\phi }\right)\right)\right)$
113 103 112 mpcom ${⊢}{V}{G}{E}\to \left(\left|{V}\right|={n}\to \left(\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)\to {\psi }\right)\to {\phi }\right)\right)$
114 113 imp ${⊢}\left({V}{G}{E}\wedge \left|{V}\right|={n}\right)\to \left(\forall {v}\phantom{\rule{.4em}{0ex}}\forall {e}\phantom{\rule{.4em}{0ex}}\left(\left({v}{G}{e}\wedge \left|{v}\right|={n}\right)\to {\psi }\right)\to {\phi }\right)$
115 100 114 syl5 ${⊢}\left({V}{G}{E}\wedge \left|{V}\right|={n}\right)\to \left({n}\in {ℕ}_{0}\to {\phi }\right)$
116 115 expcom ${⊢}\left|{V}\right|={n}\to \left({V}{G}{E}\to \left({n}\in {ℕ}_{0}\to {\phi }\right)\right)$
117 116 com23 ${⊢}\left|{V}\right|={n}\to \left({n}\in {ℕ}_{0}\to \left({V}{G}{E}\to {\phi }\right)\right)$
118 117 eqcoms ${⊢}{n}=\left|{V}\right|\to \left({n}\in {ℕ}_{0}\to \left({V}{G}{E}\to {\phi }\right)\right)$
119 118 imp ${⊢}\left({n}=\left|{V}\right|\wedge {n}\in {ℕ}_{0}\right)\to \left({V}{G}{E}\to {\phi }\right)$
120 119 exlimiv ${⊢}\exists {n}\phantom{\rule{.4em}{0ex}}\left({n}=\left|{V}\right|\wedge {n}\in {ℕ}_{0}\right)\to \left({V}{G}{E}\to {\phi }\right)$
121 10 120 sylbi ${⊢}\left|{V}\right|\in {ℕ}_{0}\to \left({V}{G}{E}\to {\phi }\right)$
122 9 121 syl ${⊢}{V}\in \mathrm{Fin}\to \left({V}{G}{E}\to {\phi }\right)$
123 122 impcom ${⊢}\left({V}{G}{E}\wedge {V}\in \mathrm{Fin}\right)\to {\phi }$