Metamath Proof Explorer

Theorem brfi1uzind

Description: Properties of a binary relation with a finite first component with at least L elements, proven by finite induction on the size of the first component. This theorem can be applied for graphs (as binary relation between the set of vertices and an edge function) with a finite number of vertices, usually with L = 0 (see brfi1ind ) or L = 1 . (Contributed by Alexander van der Vekens, 7-Jan-2018) (Proof shortened by AV, 23-Oct-2020) (Revised by AV, 28-Mar-2021)

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

Proof

Step Hyp Ref Expression
1 brfi1uzind.r ⊢ Rel ⁡ G
2 brfi1uzind.f ⊢ F ∈ V
3 brfi1uzind.l ⊢ L ∈ ℕ 0
4 brfi1uzind.1 ⊢ v = V ∧ e = E → ψ ↔ φ
5 brfi1uzind.2 ⊢ v = w ∧ e = f → ψ ↔ θ
6 brfi1uzind.3 ⊢ v G e ∧ n ∈ v → v ∖ n G F
7 brfi1uzind.4 ⊢ w = v ∖ n ∧ f = F → θ ↔ χ
8 brfi1uzind.base ⊢ v G e ∧ v = L → ψ
9 brfi1uzind.step ⊢ y + 1 ∈ ℕ 0 ∧ v G e ∧ v = y + 1 ∧ n ∈ v ∧ χ → ψ
10 1 brrelex12i ⊢ V G E → V ∈ V ∧ E ∈ V
11 simpl ⊢ V ∈ V ∧ E ∈ V → V ∈ V
12 simplr ⊢ V ∈ V ∧ E ∈ V ∧ a = V → E ∈ V
13 breq12 ⊢ a = V ∧ b = E → a G b ↔ V G E
14 13 adantll ⊢ V ∈ V ∧ E ∈ V ∧ a = V ∧ b = E → a G b ↔ V G E
15 12 14 sbcied ⊢ V ∈ V ∧ E ∈ V ∧ a = V → [˙E / b]˙ a G b ↔ V G E
16 11 15 sbcied ⊢ V ∈ V ∧ E ∈ V → [˙V / a]˙ [˙E / b]˙ a G b ↔ V G E
17 16 biimprcd ⊢ V G E → V ∈ V ∧ E ∈ V → [˙V / a]˙ [˙E / b]˙ a G b
18 10 17 mpd ⊢ V G E → [˙V / a]˙ [˙E / b]˙ a G b
19 vex ⊢ v ∈ V
20 vex ⊢ e ∈ V
21 breq12 ⊢ a = v ∧ b = e → a G b ↔ v G e
22 19 20 21 sbc2ie ⊢ [˙v / a]˙ [˙e / b]˙ a G b ↔ v G e
23 19 difexi ⊢ v ∖ n ∈ V
24 breq12 ⊢ a = v ∖ n ∧ b = F → a G b ↔ v ∖ n G F
25 23 2 24 sbc2ie ⊢ [˙ v ∖ n / a]˙ [˙F / b]˙ a G b ↔ v ∖ n G F
26 6 25 sylibr ⊢ v G e ∧ n ∈ v → [˙ v ∖ n / a]˙ [˙F / b]˙ a G b
27 22 26 sylanb ⊢ [˙v / a]˙ [˙e / b]˙ a G b ∧ n ∈ v → [˙ v ∖ n / a]˙ [˙F / b]˙ a G b
28 22 8 sylanb ⊢ [˙v / a]˙ [˙e / b]˙ a G b ∧ v = L → ψ
29 22 3anbi1i ⊢ [˙v / a]˙ [˙e / b]˙ a G b ∧ v = y + 1 ∧ n ∈ v ↔ v G e ∧ v = y + 1 ∧ n ∈ v
30 29 anbi2i ⊢ y + 1 ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ a G b ∧ v = y + 1 ∧ n ∈ v ↔ y + 1 ∈ ℕ 0 ∧ v G e ∧ v = y + 1 ∧ n ∈ v
31 30 9 sylanb ⊢ y + 1 ∈ ℕ 0 ∧ [˙v / a]˙ [˙e / b]˙ a G b ∧ v = y + 1 ∧ n ∈ v ∧ χ → ψ
32 2 3 4 5 27 7 28 31 fi1uzind ⊢ [˙V / a]˙ [˙E / b]˙ a G b ∧ V ∈ Fin ∧ L ≤ V → φ
33 18 32 syl3an1 ⊢ V G E ∧ V ∈ Fin ∧ L ≤ V → φ