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 RelG
brfi1uzind.f FV
brfi1uzind.l L0
brfi1uzind.1 v=Ve=Eψφ
brfi1uzind.2 v=we=fψθ
brfi1uzind.3 vGenvvnGF
brfi1uzind.4 w=vnf=Fθχ
brfi1uzind.base vGev=Lψ
brfi1uzind.step y+10vGev=y+1nvχψ
Assertion brfi1uzind VGEVFinLVφ

Proof

Step Hyp Ref Expression
1 brfi1uzind.r RelG
2 brfi1uzind.f FV
3 brfi1uzind.l L0
4 brfi1uzind.1 v=Ve=Eψφ
5 brfi1uzind.2 v=we=fψθ
6 brfi1uzind.3 vGenvvnGF
7 brfi1uzind.4 w=vnf=Fθχ
8 brfi1uzind.base vGev=Lψ
9 brfi1uzind.step y+10vGev=y+1nvχψ
10 1 brrelex12i VGEVVEV
11 simpl VVEVVV
12 simplr VVEVa=VEV
13 breq12 a=Vb=EaGbVGE
14 13 adantll VVEVa=Vb=EaGbVGE
15 12 14 sbcied VVEVa=V[˙E/b]˙aGbVGE
16 11 15 sbcied VVEV[˙V/a]˙[˙E/b]˙aGbVGE
17 16 biimprcd VGEVVEV[˙V/a]˙[˙E/b]˙aGb
18 10 17 mpd VGE[˙V/a]˙[˙E/b]˙aGb
19 vex vV
20 vex eV
21 breq12 a=vb=eaGbvGe
22 19 20 21 sbc2ie [˙v/a]˙[˙e/b]˙aGbvGe
23 19 difexi vnV
24 breq12 a=vnb=FaGbvnGF
25 23 2 24 sbc2ie [˙vn/a]˙[˙F/b]˙aGbvnGF
26 6 25 sylibr vGenv[˙vn/a]˙[˙F/b]˙aGb
27 22 26 sylanb [˙v/a]˙[˙e/b]˙aGbnv[˙vn/a]˙[˙F/b]˙aGb
28 22 8 sylanb [˙v/a]˙[˙e/b]˙aGbv=Lψ
29 22 3anbi1i [˙v/a]˙[˙e/b]˙aGbv=y+1nvvGev=y+1nv
30 29 anbi2i y+10[˙v/a]˙[˙e/b]˙aGbv=y+1nvy+10vGev=y+1nv
31 30 9 sylanb y+10[˙v/a]˙[˙e/b]˙aGbv=y+1nvχψ
32 2 3 4 5 27 7 28 31 fi1uzind [˙V/a]˙[˙E/b]˙aGbVFinLVφ
33 18 32 syl3an1 VGEVFinLVφ