Metamath Proof Explorer


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 V
opfi1ind.f F V
opfi1ind.1 v = V e = E ψ φ
opfi1ind.2 v = w e = f ψ θ
opfi1ind.3 v e G n v v n F G
opfi1ind.4 w = v n f = F θ χ
opfi1ind.base v e G v = 0 ψ
opfi1ind.step y + 1 0 v e G v = y + 1 n v χ ψ
Assertion opfi1ind V E G V Fin φ

Proof

Step Hyp Ref Expression
1 opfi1ind.e E V
2 opfi1ind.f F V
3 opfi1ind.1 v = V e = E ψ φ
4 opfi1ind.2 v = w e = f ψ θ
5 opfi1ind.3 v e G n v v n F G
6 opfi1ind.4 w = v n f = F θ χ
7 opfi1ind.base v e G v = 0 ψ
8 opfi1ind.step y + 1 0 v e G v = y + 1 n v χ ψ
9 hashge0 V Fin 0 V
10 9 adantl V E G V Fin 0 V
11 0nn0 0 0
12 1 2 11 3 4 5 6 7 8 opfi1uzind V E G V Fin 0 V φ
13 10 12 mpd3an3 V E G V Fin φ