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	$⊢ V = Vtx (G)$
	Assertion	wlkl0	$⊢ X \in V \to \{w \in ClWalks (G) \| (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)\} = \{⟨\emptyset, \{⟨0, X⟩\}⟩\}$

Proof

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

Metamath Proof Explorer

Theorem wlkl0

Proof