dfconngr1

Description: Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017) (Revised by AV, 15-Feb-2021)

		Ref	Expression
	Assertion	dfconngr1	$⊢ ConnGraph = \{g \| \underset{˙}{[} Vtx (g) / v \underset{˙}{]} \forall k \in v \forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p\}$

Proof

Step	Hyp	Ref	Expression
1		df-conngr	$⊢ ConnGraph = \{g \| \underset{˙}{[} Vtx (g) / v \underset{˙}{]} \forall k \in v \forall n \in v \exists f \exists p f (k PathsOn (g) n) p\}$
2		eqid	$⊢ Vtx (g) = Vtx (g)$
3	2	0pthonv	$⊢ k \in Vtx (g) \to \exists f \exists p f (k PathsOn (g) k) p$
4		oveq2	$⊢ n = k \to k PathsOn (g) n = k PathsOn (g) k$
5	4	breqd	$⊢ n = k \to (f (k PathsOn (g) n) p \leftrightarrow f (k PathsOn (g) k) p)$
6	5	2exbidv	$⊢ n = k \to (\exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \exists f \exists p f (k PathsOn (g) k) p)$
7	6	ralsng	$⊢ k \in Vtx (g) \to (\forall n \in \{k\} \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \exists f \exists p f (k PathsOn (g) k) p)$
8	3 7	mpbird	$⊢ k \in Vtx (g) \to \forall n \in \{k\} \exists f \exists p f (k PathsOn (g) n) p$
9		difsnid	$⊢ k \in Vtx (g) \to (Vtx (g) ∖ \{k\}) \cup \{k\} = Vtx (g)$
10	9	eqcomd	$⊢ k \in Vtx (g) \to Vtx (g) = (Vtx (g) ∖ \{k\}) \cup \{k\}$
11	10	raleqdv	$⊢ k \in Vtx (g) \to (\forall n \in Vtx (g) \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall n \in ((Vtx (g) ∖ \{k\}) \cup \{k\}) \exists f \exists p f (k PathsOn (g) n) p)$
12		ralunb	$⊢ \forall n \in ((Vtx (g) ∖ \{k\}) \cup \{k\}) \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow (\forall n \in (Vtx (g) ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p \land \forall n \in \{k\} \exists f \exists p f (k PathsOn (g) n) p)$
13	11 12	bitrdi	$⊢ k \in Vtx (g) \to (\forall n \in Vtx (g) \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow (\forall n \in (Vtx (g) ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p \land \forall n \in \{k\} \exists f \exists p f (k PathsOn (g) n) p))$
14	8 13	mpbiran2d	$⊢ k \in Vtx (g) \to (\forall n \in Vtx (g) \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall n \in (Vtx (g) ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p)$
15	14	ralbiia	$⊢ \forall k \in Vtx (g) \forall n \in Vtx (g) \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall k \in Vtx (g) \forall n \in (Vtx (g) ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p$
16		fvex	$⊢ Vtx (g) \in V$
17		raleq	$⊢ v = Vtx (g) \to (\forall n \in v \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall n \in Vtx (g) \exists f \exists p f (k PathsOn (g) n) p)$
18	17	raleqbi1dv	$⊢ v = Vtx (g) \to (\forall k \in v \forall n \in v \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall k \in Vtx (g) \forall n \in Vtx (g) \exists f \exists p f (k PathsOn (g) n) p)$
19		difeq1	$⊢ v = Vtx (g) \to v ∖ \{k\} = Vtx (g) ∖ \{k\}$
20	19	raleqdv	$⊢ v = Vtx (g) \to (\forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall n \in (Vtx (g) ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p)$
21	20	raleqbi1dv	$⊢ v = Vtx (g) \to (\forall k \in v \forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall k \in Vtx (g) \forall n \in (Vtx (g) ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p)$
22	18 21	bibi12d	$⊢ v = Vtx (g) \to ((\forall k \in v \forall n \in v \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall k \in v \forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p) \leftrightarrow (\forall k \in Vtx (g) \forall n \in Vtx (g) \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall k \in Vtx (g) \forall n \in (Vtx (g) ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p))$
23	16 22	sbcie	$⊢ \underset{˙}{[} Vtx (g) / v \underset{˙}{]} (\forall k \in v \forall n \in v \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall k \in v \forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p) \leftrightarrow (\forall k \in Vtx (g) \forall n \in Vtx (g) \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall k \in Vtx (g) \forall n \in (Vtx (g) ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p)$
24	15 23	mpbir	$⊢ \underset{˙}{[} Vtx (g) / v \underset{˙}{]} (\forall k \in v \forall n \in v \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall k \in v \forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p)$
25		sbcbi1	$⊢ \underset{˙}{[} Vtx (g) / v \underset{˙}{]} (\forall k \in v \forall n \in v \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \forall k \in v \forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p) \to (\underset{˙}{[} Vtx (g) / v \underset{˙}{]} \forall k \in v \forall n \in v \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \underset{˙}{[} Vtx (g) / v \underset{˙}{]} \forall k \in v \forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p)$
26	24 25	ax-mp	$⊢ \underset{˙}{[} Vtx (g) / v \underset{˙}{]} \forall k \in v \forall n \in v \exists f \exists p f (k PathsOn (g) n) p \leftrightarrow \underset{˙}{[} Vtx (g) / v \underset{˙}{]} \forall k \in v \forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p$
27	26	abbii	$⊢ \{g \| \underset{˙}{[} Vtx (g) / v \underset{˙}{]} \forall k \in v \forall n \in v \exists f \exists p f (k PathsOn (g) n) p\} = \{g \| \underset{˙}{[} Vtx (g) / v \underset{˙}{]} \forall k \in v \forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p\}$
28	1 27	eqtri	$⊢ ConnGraph = \{g \| \underset{˙}{[} Vtx (g) / v \underset{˙}{]} \forall k \in v \forall n \in (v ∖ \{k\}) \exists f \exists p f (k PathsOn (g) n) p\}$

Metamath Proof Explorer

Theorem dfconngr1

Proof