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	biimpi	$⊢ \|1^{st} (w)\| = 0 \to 1^{st} (w) = \emptyset$
9	8	adantr	$⊢ (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X) \to 1^{st} (w) = \emptyset$
10	9	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$
11	9	adantl	$⊢ (X \in V \land (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)) \to 1^{st} (w) = \emptyset$
12	11	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))$
13	1	1vgrex	$⊢ X \in V \to G \in V$
14	1	0clwlk	$⊢ G \in V \to (\emptyset ClWalks (G) 2^{nd} (w) \leftrightarrow 2^{nd} (w) : (0 \dots 0) ⟶ V)$
15	13 14	syl	$⊢ X \in V \to (\emptyset ClWalks (G) 2^{nd} (w) \leftrightarrow 2^{nd} (w) : (0 \dots 0) ⟶ V)$
16	15	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)$
17	12 16	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)$
18		fz0sn	$⊢ (0 \dots 0) = \{0\}$
19	18	feq2i	$⊢ 2^{nd} (w) : (0 \dots 0) ⟶ V \leftrightarrow 2^{nd} (w) : \{0\} ⟶ V$
20		c0ex	$⊢ 0 \in V$
21	20	fsn2	$⊢ 2^{nd} (w) : \{0\} ⟶ V \leftrightarrow (2^{nd} (w) (0) \in V \land 2^{nd} (w) = \{⟨0, 2^{nd} (w) (0)⟩\})$
22		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)⟩\}$
23		simprr	$⊢ (X \in V \land (\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X)) \to 2^{nd} (w) (0) = X$
24	23	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$
25	24	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⟩$
26	25	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⟩\}$
27	22 26	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⟩\}$
28	27	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⟩\})$
29	21 28	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⟩\})$
30	19 29	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⟩\})$
31	17 30	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⟩\})$
32	31	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⟩\}))$
33	32	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⟩\}))$
34	33	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⟩\}$
35	10 34	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⟩\}⟩$
36	35	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⟩\}⟩))$
37		eleq1	$⊢ w = ⟨1^{st} (w), 2^{nd} (w)⟩ \to (w \in ClWalks (G) \leftrightarrow ⟨1^{st} (w), 2^{nd} (w)⟩ \in ClWalks (G))$
38		df-br	$⊢ 1^{st} (w) ClWalks (G) 2^{nd} (w) \leftrightarrow ⟨1^{st} (w), 2^{nd} (w)⟩ \in ClWalks (G)$
39	37 38	bitr4di	$⊢ w = ⟨1^{st} (w), 2^{nd} (w)⟩ \to (w \in ClWalks (G) \leftrightarrow 1^{st} (w) ClWalks (G) 2^{nd} (w))$
40		eqeq1	$⊢ w = ⟨1^{st} (w), 2^{nd} (w)⟩ \to (w = ⟨\emptyset, \{⟨0, X⟩\}⟩ \leftrightarrow ⟨1^{st} (w), 2^{nd} (w)⟩ = ⟨\emptyset, \{⟨0, X⟩\}⟩)$
41	40	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⟩\}⟩))$
42	39 41	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⟩\}⟩)))$
43	36 42	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⟩\}⟩)))$
44	43	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⟩\}⟩)))$
45	4 44	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⟩\}⟩))$
46	45	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⟩\}⟩))$
47	46	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⟩\}⟩)$
48		eqidd	$⊢ X \in V \to \emptyset = \emptyset$
49	20	a1i	$⊢ X \in V \to 0 \in V$
50		snidg	$⊢ X \in V \to X \in \{X\}$
51	49 50	fsnd	$⊢ X \in V \to \{⟨0, X⟩\} : \{0\} ⟶ \{X\}$
52	1	0clwlkv	$⊢ (X \in V \land \emptyset = \emptyset \land \{⟨0, X⟩\} : \{0\} ⟶ \{X\}) \to \emptyset ClWalks (G) \{⟨0, X⟩\}$
53	48 51 52	mpd3an23	$⊢ X \in V \to \emptyset ClWalks (G) \{⟨0, X⟩\}$
54		hash0	$⊢ \|\emptyset\| = 0$
55	54	a1i	$⊢ X \in V \to \|\emptyset\| = 0$
56		fvsng	$⊢ (0 \in V \land X \in V) \to \{⟨0, X⟩\} (0) = X$
57	20 56	mpan	$⊢ X \in V \to \{⟨0, X⟩\} (0) = X$
58	53 55 57	jca32	$⊢ X \in V \to (\emptyset ClWalks (G) \{⟨0, X⟩\} \land (\|\emptyset\| = 0 \land \{⟨0, X⟩\} (0) = X))$
59		eleq1	$⊢ w = ⟨\emptyset, \{⟨0, X⟩\}⟩ \to (w \in ClWalks (G) \leftrightarrow ⟨\emptyset, \{⟨0, X⟩\}⟩ \in ClWalks (G))$
60		df-br	$⊢ \emptyset ClWalks (G) \{⟨0, X⟩\} \leftrightarrow ⟨\emptyset, \{⟨0, X⟩\}⟩ \in ClWalks (G)$
61	59 60	bitr4di	$⊢ w = ⟨\emptyset, \{⟨0, X⟩\}⟩ \to (w \in ClWalks (G) \leftrightarrow \emptyset ClWalks (G) \{⟨0, X⟩\})$
62		0ex	$⊢ \emptyset \in V$
63		snex	$⊢ \{⟨0, X⟩\} \in V$
64	62 63	op1std	$⊢ w = ⟨\emptyset, \{⟨0, X⟩\}⟩ \to 1^{st} (w) = \emptyset$
65	64	fveqeq2d	$⊢ w = ⟨\emptyset, \{⟨0, X⟩\}⟩ \to (\|1^{st} (w)\| = 0 \leftrightarrow \|\emptyset\| = 0)$
66	62 63	op2ndd	$⊢ w = ⟨\emptyset, \{⟨0, X⟩\}⟩ \to 2^{nd} (w) = \{⟨0, X⟩\}$
67	66	fveq1d	$⊢ w = ⟨\emptyset, \{⟨0, X⟩\}⟩ \to 2^{nd} (w) (0) = \{⟨0, X⟩\} (0)$
68	67	eqeq1d	$⊢ w = ⟨\emptyset, \{⟨0, X⟩\}⟩ \to (2^{nd} (w) (0) = X \leftrightarrow \{⟨0, X⟩\} (0) = X)$
69	65 68	anbi12d	$⊢ w = ⟨\emptyset, \{⟨0, X⟩\}⟩ \to ((\|1^{st} (w)\| = 0 \land 2^{nd} (w) (0) = X) \leftrightarrow (\|\emptyset\| = 0 \land \{⟨0, X⟩\} (0) = X))$
70	61 69	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)))$
71	58 70	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)))$
72	47 71	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⟩\}⟩)$
73	72	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⟩\}⟩)$
74		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⟩\}⟩)$
75	73 74	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