# Metamath Proof Explorer

## Theorem opfi1uzind

Description: Properties of an ordered pair 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 (represented as orderd pairs of vertices and edges) with a finite number of vertices, usually with L = 0 (see opfi1ind ) or L = 1 . (Contributed by AV, 22-Oct-2020) (Revised by AV, 28-Mar-2021)

Ref Expression
Hypotheses opfi1uzind.e ${⊢}{E}\in \mathrm{V}$
opfi1uzind.f ${⊢}{F}\in \mathrm{V}$
opfi1uzind.l ${⊢}{L}\in {ℕ}_{0}$
opfi1uzind.1 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({\psi }↔{\phi }\right)$
opfi1uzind.2 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({\psi }↔{\theta }\right)$
opfi1uzind.3 ${⊢}\left(⟨{v},{e}⟩\in {G}\wedge {n}\in {v}\right)\to ⟨{v}\setminus \left\{{n}\right\},{F}⟩\in {G}$
opfi1uzind.4 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({\theta }↔{\chi }\right)$
opfi1uzind.base ${⊢}\left(⟨{v},{e}⟩\in {G}\wedge \left|{v}\right|={L}\right)\to {\psi }$
opfi1uzind.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 opfi1uzind ${⊢}\left(⟨{V},{E}⟩\in {G}\wedge {V}\in \mathrm{Fin}\wedge {L}\le \left|{V}\right|\right)\to {\phi }$

### Proof

Step Hyp Ref Expression
1 opfi1uzind.e ${⊢}{E}\in \mathrm{V}$
2 opfi1uzind.f ${⊢}{F}\in \mathrm{V}$
3 opfi1uzind.l ${⊢}{L}\in {ℕ}_{0}$
4 opfi1uzind.1 ${⊢}\left({v}={V}\wedge {e}={E}\right)\to \left({\psi }↔{\phi }\right)$
5 opfi1uzind.2 ${⊢}\left({v}={w}\wedge {e}={f}\right)\to \left({\psi }↔{\theta }\right)$
6 opfi1uzind.3 ${⊢}\left(⟨{v},{e}⟩\in {G}\wedge {n}\in {v}\right)\to ⟨{v}\setminus \left\{{n}\right\},{F}⟩\in {G}$
7 opfi1uzind.4 ${⊢}\left({w}={v}\setminus \left\{{n}\right\}\wedge {f}={F}\right)\to \left({\theta }↔{\chi }\right)$
8 opfi1uzind.base ${⊢}\left(⟨{v},{e}⟩\in {G}\wedge \left|{v}\right|={L}\right)\to {\psi }$
9 opfi1uzind.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 }$
10 1 a1i ${⊢}{a}={V}\to {E}\in \mathrm{V}$
11 opeq12 ${⊢}\left({a}={V}\wedge {b}={E}\right)\to ⟨{a},{b}⟩=⟨{V},{E}⟩$
12 11 eleq1d ${⊢}\left({a}={V}\wedge {b}={E}\right)\to \left(⟨{a},{b}⟩\in {G}↔⟨{V},{E}⟩\in {G}\right)$
13 10 12 sbcied
14 13 sbcieg
15 14 biimparc
17 vex ${⊢}{v}\in \mathrm{V}$
18 vex ${⊢}{e}\in \mathrm{V}$
19 opeq12 ${⊢}\left({a}={v}\wedge {b}={e}\right)\to ⟨{a},{b}⟩=⟨{v},{e}⟩$
20 19 eleq1d ${⊢}\left({a}={v}\wedge {b}={e}\right)\to \left(⟨{a},{b}⟩\in {G}↔⟨{v},{e}⟩\in {G}\right)$
21 17 18 20 sbc2ie
22 21 6 sylanb
23 17 difexi ${⊢}{v}\setminus \left\{{n}\right\}\in \mathrm{V}$
24 opeq12 ${⊢}\left({a}={v}\setminus \left\{{n}\right\}\wedge {b}={F}\right)\to ⟨{a},{b}⟩=⟨{v}\setminus \left\{{n}\right\},{F}⟩$
25 24 eleq1d ${⊢}\left({a}={v}\setminus \left\{{n}\right\}\wedge {b}={F}\right)\to \left(⟨{a},{b}⟩\in {G}↔⟨{v}\setminus \left\{{n}\right\},{F}⟩\in {G}\right)$
26 23 2 25 sbc2ie
27 22 26 sylibr
28 21 8 sylanb
29 21 3anbi1i
30 29 anbi2i
31 30 9 sylanb
32 2 3 4 5 27 7 28 31 fi1uzind
33 16 32 syld3an1 ${⊢}\left(⟨{V},{E}⟩\in {G}\wedge {V}\in \mathrm{Fin}\wedge {L}\le \left|{V}\right|\right)\to {\phi }$