Theorem opfi1ind

Description: Properties of an ordered pair with a finite first component, 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, e.g., fusgrfis . (Contributed by AV, 22-Oct-2020) (Revised by AV, 28-Mar-2021)

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

Proof

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