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 𝐺 | |
| brfi1ind.f | ⊢ 𝐹 ∈ V | ||
| brfi1ind.1 | ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜓 ↔ 𝜑 ) ) | ||
| brfi1ind.2 | ⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝜓 ↔ 𝜃 ) ) | ||
| brfi1ind.3 | ⊢ ( ( 𝑣 𝐺 𝑒 ∧ 𝑛 ∈ 𝑣 ) → ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) | ||
| brfi1ind.4 | ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝜃 ↔ 𝜒 ) ) | ||
| brfi1ind.base | ⊢ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝜓 ) | ||
| brfi1ind.step | ⊢ ( ( ( ( 𝑦 + 1 ) ∈ ℕ0 ∧ ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = ( 𝑦 + 1 ) ∧ 𝑛 ∈ 𝑣 ) ) ∧ 𝜒 ) → 𝜓 ) | ||
| Assertion | brfi1ind | ⊢ ( ( 𝑉 𝐺 𝐸 ∧ 𝑉 ∈ Fin ) → 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | brfi1ind.r | ⊢ Rel 𝐺 | |
| 2 | brfi1ind.f | ⊢ 𝐹 ∈ V | |
| 3 | brfi1ind.1 | ⊢ ( ( 𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ) → ( 𝜓 ↔ 𝜑 ) ) | |
| 4 | brfi1ind.2 | ⊢ ( ( 𝑣 = 𝑤 ∧ 𝑒 = 𝑓 ) → ( 𝜓 ↔ 𝜃 ) ) | |
| 5 | brfi1ind.3 | ⊢ ( ( 𝑣 𝐺 𝑒 ∧ 𝑛 ∈ 𝑣 ) → ( 𝑣 ∖ { 𝑛 } ) 𝐺 𝐹 ) | |
| 6 | brfi1ind.4 | ⊢ ( ( 𝑤 = ( 𝑣 ∖ { 𝑛 } ) ∧ 𝑓 = 𝐹 ) → ( 𝜃 ↔ 𝜒 ) ) | |
| 7 | brfi1ind.base | ⊢ ( ( 𝑣 𝐺 𝑒 ∧ ( ♯ ‘ 𝑣 ) = 0 ) → 𝜓 ) | |
| 8 | brfi1ind.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 | brfi1uzind | ⊢ ( ( 𝑉 𝐺 𝐸 ∧ 𝑉 ∈ Fin ∧ 0 ≤ ( ♯ ‘ 𝑉 ) ) → 𝜑 ) |
| 13 | 10 12 | mpd3an3 | ⊢ ( ( 𝑉 𝐺 𝐸 ∧ 𝑉 ∈ Fin ) → 𝜑 ) |