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 ⊢vGe∧n∈v→v∖nGF
brfi1ind.4 ⊢w=v∖n∧f=F→θ↔χ
brfi1ind.base ⊢vGe∧v=0→ψ
brfi1ind.step ⊢y+1∈ℕ0∧vGe∧v=y+1∧n∈v∧χ→ψ
Assertion brfi1ind ⊢VGE∧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 ⊢vGe∧n∈v→v∖nGF
6 brfi1ind.4 ⊢w=v∖n∧f=F→θ↔χ
7 brfi1ind.base ⊢vGe∧v=0→ψ
8 brfi1ind.step ⊢y+1∈ℕ0∧vGe∧v=y+1∧n∈v∧χ→ψ
9 hashge0 ⊢V∈Fin→0≤V
10 9 adantl ⊢VGE∧V∈Fin→0≤V
11 0nn0 ⊢0∈ℕ0
12 1 2 11 3 4 5 6 7 8 brfi1uzind ⊢VGE∧V∈Fin∧0≤V→φ
13 10 12 mpd3an3 ⊢VGE∧V∈Fin→φ