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

Metamath Proof Explorer

Theorem wlkl0

Proof