# 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}\in \mathrm{V}$
opfi1ind.f ${⊢}{F}\in \mathrm{V}$
opfi1ind.1 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({\psi }↔{\phi }\right)$
opfi1ind.2 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({\psi }↔{\theta }\right)$
opfi1ind.3 ${⊢}\left(⟨{v},{e}⟩\in {G}\wedge {n}\in {v}\right)\to ⟨{v}\setminus \left\{{n}\right\},{F}⟩\in {G}$
opfi1ind.4 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({\theta }↔{\chi }\right)$
opfi1ind.base ${⊢}\left(⟨{v},{e}⟩\in {G}\wedge \left|{v}\right|=0\right)\to {\psi }$
opfi1ind.step ${⊢}\left(\left({y}+1\in {ℕ}_{0}\wedge \left(⟨{v},{e}⟩\in {G}\wedge \left|{v}\right|={y}+1\wedge {n}\in {v}\right)\right)\wedge {\chi }\right)\to {\psi }$
Assertion opfi1ind ${⊢}\left(⟨{V},{E}⟩\in {G}\wedge {V}\in \mathrm{Fin}\right)\to {\phi }$

### Proof

Step Hyp Ref Expression
1 opfi1ind.e ${⊢}{E}\in \mathrm{V}$
2 opfi1ind.f ${⊢}{F}\in \mathrm{V}$
3 opfi1ind.1 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({\psi }↔{\phi }\right)$
4 opfi1ind.2 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({\psi }↔{\theta }\right)$
5 opfi1ind.3 ${⊢}\left(⟨{v},{e}⟩\in {G}\wedge {n}\in {v}\right)\to ⟨{v}\setminus \left\{{n}\right\},{F}⟩\in {G}$
6 opfi1ind.4 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({\theta }↔{\chi }\right)$
7 opfi1ind.base ${⊢}\left(⟨{v},{e}⟩\in {G}\wedge \left|{v}\right|=0\right)\to {\psi }$
8 opfi1ind.step ${⊢}\left(\left({y}+1\in {ℕ}_{0}\wedge \left(⟨{v},{e}⟩\in {G}\wedge \left|{v}\right|={y}+1\wedge {n}\in {v}\right)\right)\wedge {\chi }\right)\to {\psi }$
9 hashge0 ${⊢}{V}\in \mathrm{Fin}\to 0\le \left|{V}\right|$
10 9 adantl ${⊢}\left(⟨{V},{E}⟩\in {G}\wedge {V}\in \mathrm{Fin}\right)\to 0\le \left|{V}\right|$
11 0nn0 ${⊢}0\in {ℕ}_{0}$
12 1 2 11 3 4 5 6 7 8 opfi1uzind ${⊢}\left(⟨{V},{E}⟩\in {G}\wedge {V}\in \mathrm{Fin}\wedge 0\le \left|{V}\right|\right)\to {\phi }$
13 10 12 mpd3an3 ${⊢}\left(⟨{V},{E}⟩\in {G}\wedge {V}\in \mathrm{Fin}\right)\to {\phi }$