This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brfi1ind

Description: Properties of a binary relation with a finite first component, proven by finite induction on the size of the first component. (Contributed by Alexander van der Vekens, 7-Jan-2018) (Revised by AV, 28-Mar-2021)

Ref Expression
Hypotheses brfi1ind.r ⊢ Rel ⁡ G
brfi1ind.f ⊢ F ∈ V
brfi1ind.1 ⊢ v = V ∧ e = E → ψ ↔ φ
brfi1ind.2 ⊢ v = w ∧ e = f → ψ ↔ θ
brfi1ind.3 ⊢ v G e ∧ n ∈ v → v ∖ n G F
brfi1ind.4 ⊢ w = v ∖ n ∧ f = F → θ ↔ χ
brfi1ind.base ⊢ v G e ∧ v = 0 → ψ
brfi1ind.step ⊢ y + 1 ∈ ℕ 0 ∧ v G e ∧ v = y + 1 ∧ n ∈ v ∧ χ → ψ
Assertion brfi1ind ⊢ V G E ∧ V ∈ Fin → φ

Proof

Step Hyp Ref Expression
1 brfi1ind.r ⊢ Rel ⁡ G
2 brfi1ind.f ⊢ F ∈ V
3 brfi1ind.1 ⊢ v = V ∧ e = E → ψ ↔ φ
4 brfi1ind.2 ⊢ v = w ∧ e = f → ψ ↔ θ
5 brfi1ind.3 ⊢ v G e ∧ n ∈ v → v ∖ n G F
6 brfi1ind.4 ⊢ w = v ∖ n ∧ f = F → θ ↔ χ
7 brfi1ind.base ⊢ v G e ∧ v = 0 → ψ
8 brfi1ind.step ⊢ y + 1 ∈ ℕ 0 ∧ v G e ∧ v = y + 1 ∧ n ∈ v ∧ χ → ψ
9 hashge0 ⊢ V ∈ Fin → 0 ≤ V
10 9 adantl ⊢ V G E ∧ V ∈ Fin → 0 ≤ V
11 0nn0 ⊢ 0 ∈ ℕ 0
12 1 2 11 3 4 5 6 7 8 brfi1uzind ⊢ V G E ∧ V ∈ Fin ∧ 0 ≤ V → φ
13 10 12 mpd3an3 ⊢ V G E ∧ V ∈ Fin → φ