wlkl0

Description: There is exactly one walk of length 0 on each vertex X . (Contributed by AV, 4-Jun-2022)

		Ref	Expression
	Hypothesis	clwlknon2num.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	Assertion	wlkl0	⊢ ( 𝑋 ∈ 𝑉 → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } = { ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		clwlknon2num.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		clwlkwlk	⊢ ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) → 𝑤 ∈ ( Walks ‘ 𝐺 ) )
3		wlkop	⊢ ( 𝑤 ∈ ( Walks ‘ 𝐺 ) → 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
4	2 3	syl	⊢ ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) → 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ )
5		fvex	⊢ ( 1^st ‘ 𝑤 ) ∈ V
6		hasheq0	⊢ ( ( 1^st ‘ 𝑤 ) ∈ V → ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ↔ ( 1^st ‘ 𝑤 ) = ∅ ) )
7	5 6	ax-mp	⊢ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ↔ ( 1^st ‘ 𝑤 ) = ∅ )
8	7	birani	⊢ ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → ( 1^st ‘ 𝑤 ) = ∅ )
9	8	3ad2ant3	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( 1^st ‘ 𝑤 ) = ∅ )
10	8	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( 1^st ‘ 𝑤 ) = ∅ )
11	10	breq1d	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ↔ ∅ ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ) )
12	1	1vgrex	⊢ ( 𝑋 ∈ 𝑉 → 𝐺 ∈ V )
13	1	0clwlk	⊢ ( 𝐺 ∈ V → ( ∅ ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ↔ ( 2^nd ‘ 𝑤 ) : ( 0 ... 0 ) ⟶ 𝑉 ) )
14	12 13	syl	⊢ ( 𝑋 ∈ 𝑉 → ( ∅ ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ↔ ( 2^nd ‘ 𝑤 ) : ( 0 ... 0 ) ⟶ 𝑉 ) )
15	14	adantr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( ∅ ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ↔ ( 2^nd ‘ 𝑤 ) : ( 0 ... 0 ) ⟶ 𝑉 ) )
16	11 15	bitrd	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ↔ ( 2^nd ‘ 𝑤 ) : ( 0 ... 0 ) ⟶ 𝑉 ) )
17		fz0sn	⊢ ( 0 ... 0 ) = { 0 }
18	17	feq2i	⊢ ( ( 2^nd ‘ 𝑤 ) : ( 0 ... 0 ) ⟶ 𝑉 ↔ ( 2^nd ‘ 𝑤 ) : { 0 } ⟶ 𝑉 )
19		c0ex	⊢ 0 ∈ V
20	19	fsn2	⊢ ( ( 2^nd ‘ 𝑤 ) : { 0 } ⟶ 𝑉 ↔ ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ⟩ } ) )
21		simprr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ∧ ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ⟩ } ) ) → ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ⟩ } )
22		simprr	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 )
23	22	adantr	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ∧ ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ⟩ } ) ) → ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 )
24	23	opeq2d	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ∧ ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ⟩ } ) ) → ⟨ 0 , ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ⟩ = ⟨ 0 , 𝑋 ⟩ )
25	24	sneqd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ∧ ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ⟩ } ) ) → { ⟨ 0 , ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ⟩ } = { ⟨ 0 , 𝑋 ⟩ } )
26	21 25	eqtrd	⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ∧ ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ⟩ } ) ) → ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , 𝑋 ⟩ } )
27	26	ex	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ∈ 𝑉 ∧ ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) ⟩ } ) → ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , 𝑋 ⟩ } ) )
28	20 27	biimtrid	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( ( 2^nd ‘ 𝑤 ) : { 0 } ⟶ 𝑉 → ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , 𝑋 ⟩ } ) )
29	18 28	biimtrid	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( ( 2^nd ‘ 𝑤 ) : ( 0 ... 0 ) ⟶ 𝑉 → ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , 𝑋 ⟩ } ) )
30	16 29	sylbid	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) → ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , 𝑋 ⟩ } ) )
31	30	ex	⊢ ( 𝑋 ∈ 𝑉 → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → ( ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) → ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , 𝑋 ⟩ } ) ) )
32	31	com23	⊢ ( 𝑋 ∈ 𝑉 → ( ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , 𝑋 ⟩ } ) ) )
33	32	3imp	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , 𝑋 ⟩ } )
34	9 33	opeq12d	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ )
35	34	3exp	⊢ ( 𝑋 ∈ 𝑉 → ( ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) ) )
36		eleq1	⊢ ( 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ → ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ↔ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) )
37		df-br	⊢ ( ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ↔ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) )
38	36 37	bitr4di	⊢ ( 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ → ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ↔ ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) ) )
39		eqeq1	⊢ ( 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ → ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ↔ ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) )
40	39	imbi2d	⊢ ( 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ → ( ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) ↔ ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) ) )
41	38 40	imbi12d	⊢ ( 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ → ( ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) ) ↔ ( ( 1^st ‘ 𝑤 ) ( ClWalks ‘ 𝐺 ) ( 2^nd ‘ 𝑤 ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) ) ) )
42	35 41	imbitrrid	⊢ ( 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ → ( 𝑋 ∈ 𝑉 → ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) ) ) )
43	42	com23	⊢ ( 𝑤 = ⟨ ( 1^st ‘ 𝑤 ) , ( 2^nd ‘ 𝑤 ) ⟩ → ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) → ( 𝑋 ∈ 𝑉 → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) ) ) )
44	4 43	mpcom	⊢ ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) → ( 𝑋 ∈ 𝑉 → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) ) )
45	44	com12	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) → 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) ) )
46	45	impd	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) → 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) )
47		eqidd	⊢ ( 𝑋 ∈ 𝑉 → ∅ = ∅ )
48	19	a1i	⊢ ( 𝑋 ∈ 𝑉 → 0 ∈ V )
49		snidg	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
50	48 49	fsnd	⊢ ( 𝑋 ∈ 𝑉 → { ⟨ 0 , 𝑋 ⟩ } : { 0 } ⟶ { 𝑋 } )
51	1	0clwlkv	⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∅ = ∅ ∧ { ⟨ 0 , 𝑋 ⟩ } : { 0 } ⟶ { 𝑋 } ) → ∅ ( ClWalks ‘ 𝐺 ) { ⟨ 0 , 𝑋 ⟩ } )
52	47 50 51	mpd3an23	⊢ ( 𝑋 ∈ 𝑉 → ∅ ( ClWalks ‘ 𝐺 ) { ⟨ 0 , 𝑋 ⟩ } )
53		hash0	⊢ ( ♯ ‘ ∅ ) = 0
54	53	a1i	⊢ ( 𝑋 ∈ 𝑉 → ( ♯ ‘ ∅ ) = 0 )
55		fvsng	⊢ ( ( 0 ∈ V ∧ 𝑋 ∈ 𝑉 ) → ( { ⟨ 0 , 𝑋 ⟩ } ‘ 0 ) = 𝑋 )
56	19 55	mpan	⊢ ( 𝑋 ∈ 𝑉 → ( { ⟨ 0 , 𝑋 ⟩ } ‘ 0 ) = 𝑋 )
57	52 54 56	jca32	⊢ ( 𝑋 ∈ 𝑉 → ( ∅ ( ClWalks ‘ 𝐺 ) { ⟨ 0 , 𝑋 ⟩ } ∧ ( ( ♯ ‘ ∅ ) = 0 ∧ ( { ⟨ 0 , 𝑋 ⟩ } ‘ 0 ) = 𝑋 ) ) )
58		eleq1	⊢ ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ → ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ↔ ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) )
59		df-br	⊢ ( ∅ ( ClWalks ‘ 𝐺 ) { ⟨ 0 , 𝑋 ⟩ } ↔ ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ∈ ( ClWalks ‘ 𝐺 ) )
60	58 59	bitr4di	⊢ ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ → ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ↔ ∅ ( ClWalks ‘ 𝐺 ) { ⟨ 0 , 𝑋 ⟩ } ) )
61		0ex	⊢ ∅ ∈ V
62		snex	⊢ { ⟨ 0 , 𝑋 ⟩ } ∈ V
63	61 62	op1std	⊢ ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ → ( 1^st ‘ 𝑤 ) = ∅ )
64	63	fveqeq2d	⊢ ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ → ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ↔ ( ♯ ‘ ∅ ) = 0 ) )
65	61 62	op2ndd	⊢ ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ → ( 2^nd ‘ 𝑤 ) = { ⟨ 0 , 𝑋 ⟩ } )
66	65	fveq1d	⊢ ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ → ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = ( { ⟨ 0 , 𝑋 ⟩ } ‘ 0 ) )
67	66	eqeq1d	⊢ ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ → ( ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ↔ ( { ⟨ 0 , 𝑋 ⟩ } ‘ 0 ) = 𝑋 ) )
68	64 67	anbi12d	⊢ ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ → ( ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ↔ ( ( ♯ ‘ ∅ ) = 0 ∧ ( { ⟨ 0 , 𝑋 ⟩ } ‘ 0 ) = 𝑋 ) ) )
69	60 68	anbi12d	⊢ ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ → ( ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ↔ ( ∅ ( ClWalks ‘ 𝐺 ) { ⟨ 0 , 𝑋 ⟩ } ∧ ( ( ♯ ‘ ∅ ) = 0 ∧ ( { ⟨ 0 , 𝑋 ⟩ } ‘ 0 ) = 𝑋 ) ) ) )
70	57 69	syl5ibrcom	⊢ ( 𝑋 ∈ 𝑉 → ( 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ → ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ) )
71	46 70	impbid	⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ↔ 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) )
72	71	alrimiv	⊢ ( 𝑋 ∈ 𝑉 → ∀ 𝑤 ( ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ↔ 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) )
73		rabeqsn	⊢ ( { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } = { ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ } ↔ ∀ 𝑤 ( ( 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∧ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) ) ↔ 𝑤 = ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ ) )
74	72 73	sylibr	⊢ ( 𝑋 ∈ 𝑉 → { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ ( ( ♯ ‘ ( 1^st ‘ 𝑤 ) ) = 0 ∧ ( ( 2^nd ‘ 𝑤 ) ‘ 0 ) = 𝑋 ) } = { ⟨ ∅ , { ⟨ 0 , 𝑋 ⟩ } ⟩ } )

Metamath Proof Explorer

Theorem wlkl0

Proof