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

Metamath Proof Explorer

Theorem opfi1uzind

Description: Properties of an ordered pair 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 (represented as ordered pairs of vertices and edges) with a finite number of vertices, usually with L = 0 (see opfi1ind ) or L = 1 . (Contributed by AV, 22-Oct-2020) (Revised by AV, 28-Mar-2021)

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

Proof

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