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	⊢ 𝐸 ∈ V
	opfi1ind.f	⊢ 𝐹 ∈ V
	opfi1ind.1	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜓 ↔ 𝜑 ) )
	opfi1ind.2	⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝜓 ↔ 𝜃 ) )
	opfi1ind.3	⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ 𝑛 ∈ 𝑣 ) → ⟨ ( 𝑣 ∖ { 𝑛 } ) , 𝐹 ⟩ ∈ 𝐺 )
	opfi1ind.4	⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝜃 ↔ 𝜒 ) )
	opfi1ind.base	⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝜓 )
	opfi1ind.step	⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ 𝜒 ) → 𝜓 )
Assertion	opfi1ind	⊢ ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin ) → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		opfi1ind.e	⊢ 𝐸 ∈ V
2		opfi1ind.f	⊢ 𝐹 ∈ V
3		opfi1ind.1	⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜓 ↔ 𝜑 ) )
4		opfi1ind.2	⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝜓 ↔ 𝜃 ) )
5		opfi1ind.3	⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ 𝑛 ∈ 𝑣 ) → ⟨ ( 𝑣 ∖ { 𝑛 } ) , 𝐹 ⟩ ∈ 𝐺 )
6		opfi1ind.4	⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝜃 ↔ 𝜒 ) )
7		opfi1ind.base	⊢ ( ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝜓 )
8		opfi1ind.step	⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( ⟨ 𝑣 , 𝑒 ⟩ ∈ 𝐺 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ 𝜒 ) → 𝜓 )
9		hashge0	⊢ ( 𝑉 ∈ Fin → 0 ≤ ( ♯ ‘ 𝑉 ) )
10	9	adantl	⊢ ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin ) → 0 ≤ ( ♯ ‘ 𝑉 ) )
11		0nn0	⊢ 0 ∈ ℕ0
12	1 2 11 3 4 5 6 7 8	opfi1uzind	⊢ ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin ∧ 0 ≤ ( ♯ ‘ 𝑉 ) ) → 𝜑 )
13	10 12	mpd3an3	⊢ ( ( ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐺 ∧ 𝑉 ∈ Fin ) → 𝜑 )