# Metamath Proof Explorer

## Theorem brfi1uzind

Description: Properties of a binary relation 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 (as binary relation between the set of vertices and an edge function) with a finite number of vertices, usually with L = 0 (see brfi1ind ) or L = 1 . (Contributed by Alexander van der Vekens, 7-Jan-2018) (Proof shortened by AV, 23-Oct-2020) (Revised by AV, 28-Mar-2021)

Ref Expression
Hypotheses brfi1uzind.r ${⊢}\mathrm{Rel}{G}$
brfi1uzind.f ${⊢}{F}\in \mathrm{V}$
brfi1uzind.l ${⊢}{L}\in {ℕ}_{0}$
brfi1uzind.1 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({\psi }↔{\phi }\right)$
brfi1uzind.2 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({\psi }↔{\theta }\right)$
brfi1uzind.3 ${⊢}\left({v}{G}{e}\wedge {n}\in {v}\right)\to \left({v}\setminus \left\{{n}\right\}\right){G}{F}$
brfi1uzind.4 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({\theta }↔{\chi }\right)$
brfi1uzind.base ${⊢}\left({v}{G}{e}\wedge \left|{v}\right|={L}\right)\to {\psi }$
brfi1uzind.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 brfi1uzind ${⊢}\left({V}{G}{E}\wedge {V}\in \mathrm{Fin}\wedge {L}\le \left|{V}\right|\right)\to {\phi }$

### Proof

Step Hyp Ref Expression
1 brfi1uzind.r ${⊢}\mathrm{Rel}{G}$
2 brfi1uzind.f ${⊢}{F}\in \mathrm{V}$
3 brfi1uzind.l ${⊢}{L}\in {ℕ}_{0}$
4 brfi1uzind.1 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({\psi }↔{\phi }\right)$
5 brfi1uzind.2 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({\psi }↔{\theta }\right)$
6 brfi1uzind.3 ${⊢}\left({v}{G}{e}\wedge {n}\in {v}\right)\to \left({v}\setminus \left\{{n}\right\}\right){G}{F}$
7 brfi1uzind.4 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({\theta }↔{\chi }\right)$
8 brfi1uzind.base ${⊢}\left({v}{G}{e}\wedge \left|{v}\right|={L}\right)\to {\psi }$
9 brfi1uzind.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 }$
10 1 brrelex12i ${⊢}{V}{G}{E}\to \left({V}\in \mathrm{V}\wedge {E}\in \mathrm{V}\right)$
11 simpl ${⊢}\left({V}\in \mathrm{V}\wedge {E}\in \mathrm{V}\right)\to {V}\in \mathrm{V}$
12 simplr ${⊢}\left(\left({V}\in \mathrm{V}\wedge {E}\in \mathrm{V}\right)\wedge {a}={V}\right)\to {E}\in \mathrm{V}$
13 breq12 ${⊢}\left({a}={V}\wedge {b}={E}\right)\to \left({a}{G}{b}↔{V}{G}{E}\right)$
14 13 adantll ${⊢}\left(\left(\left({V}\in \mathrm{V}\wedge {E}\in \mathrm{V}\right)\wedge {a}={V}\right)\wedge {b}={E}\right)\to \left({a}{G}{b}↔{V}{G}{E}\right)$
15 12 14 sbcied
16 11 15 sbcied
17 16 biimprcd
18 10 17 mpd
19 vex ${⊢}{v}\in \mathrm{V}$
20 vex ${⊢}{e}\in \mathrm{V}$
21 breq12 ${⊢}\left({a}={v}\wedge {b}={e}\right)\to \left({a}{G}{b}↔{v}{G}{e}\right)$
22 19 20 21 sbc2ie
23 19 difexi ${⊢}{v}\setminus \left\{{n}\right\}\in \mathrm{V}$
24 breq12 ${⊢}\left({a}={v}\setminus \left\{{n}\right\}\wedge {b}={F}\right)\to \left({a}{G}{b}↔\left({v}\setminus \left\{{n}\right\}\right){G}{F}\right)$
25 23 2 24 sbc2ie
26 6 25 sylibr
27 22 26 sylanb
28 22 8 sylanb
29 22 3anbi1i
30 29 anbi2i
31 30 9 sylanb
32 2 3 4 5 27 7 28 31 fi1uzind
33 18 32 syl3an1 ${⊢}\left({V}{G}{E}\wedge {V}\in \mathrm{Fin}\wedge {L}\le \left|{V}\right|\right)\to {\phi }$