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 ordered 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 {\mathbb{N}}_0$$
	opfi1uzind.1	$$⊢\left(v=V\wedge e=E\right)\to \left(\psi \leftrightarrow \phi \right)$$
	opfi1uzind.2	$$⊢\left(v=w\wedge e=f\right)\to \left(\psi \leftrightarrow \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 \leftrightarrow \chi \right)$$
	opfi1uzind.base	$$⊢\left(⟨v,e⟩\in G\wedge \left|v\right|=L\right)\to \psi$$
	opfi1uzind.step	$$⊢\left(\left(y+1\in {\mathbb{N}}_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 {\mathbb{N}}_0$$
4		opfi1uzind.1	$$⊢\left(v=V\wedge e=E\right)\to \left(\psi \leftrightarrow \phi \right)$$
5		opfi1uzind.2	$$⊢\left(v=w\wedge e=f\right)\to \left(\psi \leftrightarrow \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 \leftrightarrow \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 {\mathbb{N}}_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\leftrightarrow ⟨V,E⟩\in G\right)$$
13	10 12	sbcied	$$⊢a=V\to \left(\underset{\dot{}}{[}E/b\underset{\dot{}}{]}⟨a,b⟩\in G\leftrightarrow ⟨V,E⟩\in G\right)$$
14	13	sbcieg	$$⊢V\in \mathrm{Fin}\to \left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}⟨a,b⟩\in G\leftrightarrow ⟨V,E⟩\in G\right)$$
15	14	biimparc	$$⊢\left(⟨V,E⟩\in G\wedge V\in \mathrm{Fin}\right)\to \underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}⟨a,b⟩\in G$$
16	15	3adant3	$$⊢\left(⟨V,E⟩\in G\wedge V\in \mathrm{Fin}\wedge L\le \left|V\right|\right)\to \underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}⟨a,b⟩\in G$$
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\leftrightarrow ⟨v,e⟩\in G\right)$$
21	17 18 20	sbc2ie	$$⊢\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}⟨a,b⟩\in G\leftrightarrow ⟨v,e⟩\in G$$
22	21 6	sylanb	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}⟨a,b⟩\in G\wedge n\in v\right)\to ⟨v\setminus \left\{n\right\},F⟩\in G$$
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\leftrightarrow ⟨v\setminus \left\{n\right\},F⟩\in G\right)$$
26	23 2 25	sbc2ie	$$⊢\underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}⟨a,b⟩\in G\leftrightarrow ⟨v\setminus \left\{n\right\},F⟩\in G$$
27	22 26	sylibr	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}⟨a,b⟩\in G\wedge n\in v\right)\to \underset{\dot{}}{[}\left(v\setminus \left\{n\right\}\right)/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/b\underset{\dot{}}{]}⟨a,b⟩\in G$$
28	21 8	sylanb	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}⟨a,b⟩\in G\wedge \left|v\right|=L\right)\to \psi$$
29	21	3anbi1i	$$⊢\left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}⟨a,b⟩\in G\wedge \left|v\right|=y+1\wedge n\in v\right)\leftrightarrow \left(⟨v,e⟩\in G\wedge \left|v\right|=y+1\wedge n\in v\right)$$
30	29	anbi2i	$$⊢\left(y+1\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}⟨a,b⟩\in G\wedge \left|v\right|=y+1\wedge n\in v\right)\right)\leftrightarrow \left(y+1\in {\mathbb{N}}_0\wedge \left(⟨v,e⟩\in G\wedge \left|v\right|=y+1\wedge n\in v\right)\right)$$
31	30 9	sylanb	$$⊢\left(\left(y+1\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}v/a\underset{\dot{}}{]}\underset{\dot{}}{[}e/b\underset{\dot{}}{]}⟨a,b⟩\in G\wedge \left|v\right|=y+1\wedge n\in v\right)\right)\wedge \chi \right)\to \psi$$
32	2 3 4 5 27 7 28 31	fi1uzind	$$⊢\left(\underset{\dot{}}{[}V/a\underset{\dot{}}{]}\underset{\dot{}}{[}E/b\underset{\dot{}}{]}⟨a,b⟩\in G\wedge V\in \mathrm{Fin}\wedge L\le \left|V\right|\right)\to \phi$$
33	16 32	syld3an1	$$⊢\left(⟨V,E⟩\in G\wedge V\in \mathrm{Fin}\wedge L\le \left|V\right|\right)\to \phi$$