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 ordered 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 V$
	opfi1ind.f	$⊢ F \in V$
	opfi1ind.1	$⊢ (v = V \land e = E) \to (ψ \leftrightarrow φ)$
	opfi1ind.2	$⊢ (v = w \land e = f) \to (ψ \leftrightarrow θ)$
	opfi1ind.3	$⊢ (⟨v, e⟩ \in G \land n \in v) \to ⟨v ∖ \{n\}, F⟩ \in G$
	opfi1ind.4	$⊢ (w = v ∖ \{n\} \land f = F) \to (θ \leftrightarrow χ)$
	opfi1ind.base	$⊢ (⟨v, e⟩ \in G \land \|v\| = 0) \to ψ$
	opfi1ind.step	$⊢ ((y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in G \land \|v\| = y + 1 \land n \in v)) \land χ) \to ψ$
Assertion	opfi1ind	$⊢ (⟨V, E⟩ \in G \land V \in Fin) \to φ$

Proof

Step	Hyp	Ref	Expression
1		opfi1ind.e	$⊢ E \in V$
2		opfi1ind.f	$⊢ F \in V$
3		opfi1ind.1	$⊢ (v = V \land e = E) \to (ψ \leftrightarrow φ)$
4		opfi1ind.2	$⊢ (v = w \land e = f) \to (ψ \leftrightarrow θ)$
5		opfi1ind.3	$⊢ (⟨v, e⟩ \in G \land n \in v) \to ⟨v ∖ \{n\}, F⟩ \in G$
6		opfi1ind.4	$⊢ (w = v ∖ \{n\} \land f = F) \to (θ \leftrightarrow χ)$
7		opfi1ind.base	$⊢ (⟨v, e⟩ \in G \land \|v\| = 0) \to ψ$
8		opfi1ind.step	$⊢ ((y + 1 \in ℕ_{0} \land (⟨v, e⟩ \in G \land \|v\| = y + 1 \land n \in v)) \land χ) \to ψ$
9		hashge0	$⊢ V \in Fin \to 0 \leq \|V\|$
10	9	adantl	$⊢ (⟨V, E⟩ \in G \land V \in Fin) \to 0 \leq \|V\|$
11		0nn0	$⊢ 0 \in ℕ_{0}$
12	1 2 11 3 4 5 6 7 8	opfi1uzind	$⊢ (⟨V, E⟩ \in G \land V \in Fin \land 0 \leq \|V\|) \to φ$
13	10 12	mpd3an3	$⊢ (⟨V, E⟩ \in G \land V \in Fin) \to φ$

Metamath Proof Explorer

Theorem opfi1ind

Proof