wlkv0

Description: If there is a walk in the null graph (a class without vertices), it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018) (Revised by AV, 5-Mar-2021)

		Ref	Expression
	Assertion	wlkv0	⊢ ( ( ( Vtx ‘ 𝐺 ) = ∅ ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 1^st ‘ 𝑊 ) = ∅ ∧ ( 2^nd ‘ 𝑊 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		wlkcpr	⊢ ( 𝑊 ∈ ( Walks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) )
2		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3	2	wlkf	⊢ ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) → ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) )
4		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
5	4	wlkp	⊢ ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) → ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) )
6	3 5	jca	⊢ ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) → ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) )
7		feq3	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ∅ ) )
8		f00	⊢ ( ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ∅ ↔ ( ( 2^nd ‘ 𝑊 ) = ∅ ∧ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ ) )
9	7 8	bitrdi	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ↔ ( ( 2^nd ‘ 𝑊 ) = ∅ ∧ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ ) ) )
10		0z	⊢ 0 ∈ ℤ
11		nn0z	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ∈ ℕ₀ → ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ∈ ℤ )
12		fzn	⊢ ( ( 0 ∈ ℤ ∧ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ∈ ℤ ) → ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) < 0 ↔ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ ) )
13	10 11 12	sylancr	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ∈ ℕ₀ → ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) < 0 ↔ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ ) )
14		nn0nlt0	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ∈ ℕ₀ → ¬ ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) < 0 )
15	14	pm2.21d	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ∈ ℕ₀ → ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) < 0 → ( 1^st ‘ 𝑊 ) = ∅ ) )
16	13 15	sylbird	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ∈ ℕ₀ → ( ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ → ( 1^st ‘ 𝑊 ) = ∅ ) )
17	16	com12	⊢ ( ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ → ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ∈ ℕ₀ → ( 1^st ‘ 𝑊 ) = ∅ ) )
18	17	adantl	⊢ ( ( ( 2^nd ‘ 𝑊 ) = ∅ ∧ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ ) → ( ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ∈ ℕ₀ → ( 1^st ‘ 𝑊 ) = ∅ ) )
19		lencl	⊢ ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ∈ ℕ₀ )
20	18 19	impel	⊢ ( ( ( ( 2^nd ‘ 𝑊 ) = ∅ ∧ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ ) ∧ ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( 1^st ‘ 𝑊 ) = ∅ )
21		simpll	⊢ ( ( ( ( 2^nd ‘ 𝑊 ) = ∅ ∧ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ ) ∧ ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( 2^nd ‘ 𝑊 ) = ∅ )
22	20 21	jca	⊢ ( ( ( ( 2^nd ‘ 𝑊 ) = ∅ ∧ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ ) ∧ ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ) → ( ( 1^st ‘ 𝑊 ) = ∅ ∧ ( 2^nd ‘ 𝑊 ) = ∅ ) )
23	22	ex	⊢ ( ( ( 2^nd ‘ 𝑊 ) = ∅ ∧ ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) = ∅ ) → ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝑊 ) = ∅ ∧ ( 2^nd ‘ 𝑊 ) = ∅ ) ) )
24	9 23	biimtrdi	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) → ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) → ( ( 1^st ‘ 𝑊 ) = ∅ ∧ ( 2^nd ‘ 𝑊 ) = ∅ ) ) ) )
25	24	impcomd	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( ( ( 1^st ‘ 𝑊 ) ∈ Word dom ( iEdg ‘ 𝐺 ) ∧ ( 2^nd ‘ 𝑊 ) : ( 0 ... ( ♯ ‘ ( 1^st ‘ 𝑊 ) ) ) ⟶ ( Vtx ‘ 𝐺 ) ) → ( ( 1^st ‘ 𝑊 ) = ∅ ∧ ( 2^nd ‘ 𝑊 ) = ∅ ) ) )
26	6 25	syl5	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( ( 1^st ‘ 𝑊 ) ( Walks ‘ 𝐺 ) ( 2^nd ‘ 𝑊 ) → ( ( 1^st ‘ 𝑊 ) = ∅ ∧ ( 2^nd ‘ 𝑊 ) = ∅ ) ) )
27	1 26	biimtrid	⊢ ( ( Vtx ‘ 𝐺 ) = ∅ → ( 𝑊 ∈ ( Walks ‘ 𝐺 ) → ( ( 1^st ‘ 𝑊 ) = ∅ ∧ ( 2^nd ‘ 𝑊 ) = ∅ ) ) )
28	27	imp	⊢ ( ( ( Vtx ‘ 𝐺 ) = ∅ ∧ 𝑊 ∈ ( Walks ‘ 𝐺 ) ) → ( ( 1^st ‘ 𝑊 ) = ∅ ∧ ( 2^nd ‘ 𝑊 ) = ∅ ) )

Metamath Proof Explorer

Theorem wlkv0

Proof