Theorem brfi1ind

Description: Properties of a binary relation with a finite first component, proven by finite induction on the size of the first component. (Contributed by Alexander van der Vekens, 7-Jan-2018) (Revised by AV, 28-Mar-2021)

	Ref	Expression
Hypotheses	brfi1ind.r	|- Rel G
	brfi1ind.f	|- F e. _V
	brfi1ind.1	|- ( ( v = V /\ e = E ) -> ( ps <-> ph ) )
	brfi1ind.2	|- ( ( v = w /\ e = f ) -> ( ps <-> th ) )
	brfi1ind.3	|- ( ( v G e /\ n e. v ) -> ( v \ { n } ) G F )
	brfi1ind.4	|- ( ( w = ( v \ { n } ) /\ f = F ) -> ( th <-> ch ) )
	brfi1ind.base	|- ( ( v G e /\ ( # ` v ) = 0 ) -> ps )
	brfi1ind.step	|- ( ( ( ( y + 1 ) e. NN0 /\ ( v G e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ch ) -> ps )
Assertion	brfi1ind	|- ( ( V G E /\ V e. Fin ) -> ph )

Proof

Step	Hyp	Ref	Expression
1		brfi1ind.r	|- Rel G
2		brfi1ind.f	|- F e. _V
3		brfi1ind.1	|- ( ( v = V /\ e = E ) -> ( ps <-> ph ) )
4		brfi1ind.2	|- ( ( v = w /\ e = f ) -> ( ps <-> th ) )
5		brfi1ind.3	|- ( ( v G e /\ n e. v ) -> ( v \ { n } ) G F )
6		brfi1ind.4	|- ( ( w = ( v \ { n } ) /\ f = F ) -> ( th <-> ch ) )
7		brfi1ind.base	|- ( ( v G e /\ ( # ` v ) = 0 ) -> ps )
8		brfi1ind.step	|- ( ( ( ( y + 1 ) e. NN0 /\ ( v G e /\ ( # ` v ) = ( y + 1 ) /\ n e. v ) ) /\ ch ) -> ps )
9		hashge0	|- ( V e. Fin -> 0 <_ ( # ` V ) )
10	9	adantl	|- ( ( V G E /\ V e. Fin ) -> 0 <_ ( # ` V ) )
11		0nn0	|- 0 e. NN0
12	1 2 11 3 4 5 6 7 8	brfi1uzind	|- ( ( V G E /\ V e. Fin /\ 0 <_ ( # ` V ) ) -> ph )
13	10 12	mpd3an3	|- ( ( V G E /\ V e. Fin ) -> ph )