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 𝐸 ∈ 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 ) → 𝜑 )