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