1conngr

Description: A graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017) (Revised by AV, 15-Feb-2021)

		Ref	Expression
	Assertion	1conngr	$⊢ (G \in W \land Vtx (G) = \{N\}) \to G \in ConnGraph$

Proof

Step	Hyp	Ref	Expression
1		snidg	$⊢ N \in V \to N \in \{N\}$
2	1	adantr	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to N \in \{N\}$
3		eleq2	$⊢ Vtx (G) = \{N\} \to (N \in Vtx (G) \leftrightarrow N \in \{N\})$
4	3	ad2antll	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to (N \in Vtx (G) \leftrightarrow N \in \{N\})$
5	2 4	mpbird	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to N \in Vtx (G)$
6		eqid	$⊢ Vtx (G) = Vtx (G)$
7	6	0pthonv	$⊢ N \in Vtx (G) \to \exists f \exists p f (N PathsOn (G) N) p$
8	5 7	syl	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to \exists f \exists p f (N PathsOn (G) N) p$
9		oveq2	$⊢ n = N \to N PathsOn (G) n = N PathsOn (G) N$
10	9	breqd	$⊢ n = N \to (f (N PathsOn (G) n) p \leftrightarrow f (N PathsOn (G) N) p)$
11	10	2exbidv	$⊢ n = N \to (\exists f \exists p f (N PathsOn (G) n) p \leftrightarrow \exists f \exists p f (N PathsOn (G) N) p)$
12	11	ralsng	$⊢ N \in V \to (\forall n \in \{N\} \exists f \exists p f (N PathsOn (G) n) p \leftrightarrow \exists f \exists p f (N PathsOn (G) N) p)$
13	12	adantr	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to (\forall n \in \{N\} \exists f \exists p f (N PathsOn (G) n) p \leftrightarrow \exists f \exists p f (N PathsOn (G) N) p)$
14	8 13	mpbird	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to \forall n \in \{N\} \exists f \exists p f (N PathsOn (G) n) p$
15		oveq1	$⊢ k = N \to k PathsOn (G) n = N PathsOn (G) n$
16	15	breqd	$⊢ k = N \to (f (k PathsOn (G) n) p \leftrightarrow f (N PathsOn (G) n) p)$
17	16	2exbidv	$⊢ k = N \to (\exists f \exists p f (k PathsOn (G) n) p \leftrightarrow \exists f \exists p f (N PathsOn (G) n) p)$
18	17	ralbidv	$⊢ k = N \to (\forall n \in \{N\} \exists f \exists p f (k PathsOn (G) n) p \leftrightarrow \forall n \in \{N\} \exists f \exists p f (N PathsOn (G) n) p)$
19	18	ralsng	$⊢ N \in V \to (\forall k \in \{N\} \forall n \in \{N\} \exists f \exists p f (k PathsOn (G) n) p \leftrightarrow \forall n \in \{N\} \exists f \exists p f (N PathsOn (G) n) p)$
20	19	adantr	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to (\forall k \in \{N\} \forall n \in \{N\} \exists f \exists p f (k PathsOn (G) n) p \leftrightarrow \forall n \in \{N\} \exists f \exists p f (N PathsOn (G) n) p)$
21	14 20	mpbird	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to \forall k \in \{N\} \forall n \in \{N\} \exists f \exists p f (k PathsOn (G) n) p$
22		raleq	$⊢ Vtx (G) = \{N\} \to (\forall n \in Vtx (G) \exists f \exists p f (k PathsOn (G) n) p \leftrightarrow \forall n \in \{N\} \exists f \exists p f (k PathsOn (G) n) p)$
23	22	raleqbi1dv	$⊢ Vtx (G) = \{N\} \to (\forall k \in Vtx (G) \forall n \in Vtx (G) \exists f \exists p f (k PathsOn (G) n) p \leftrightarrow \forall k \in \{N\} \forall n \in \{N\} \exists f \exists p f (k PathsOn (G) n) p)$
24	23	ad2antll	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to (\forall k \in Vtx (G) \forall n \in Vtx (G) \exists f \exists p f (k PathsOn (G) n) p \leftrightarrow \forall k \in \{N\} \forall n \in \{N\} \exists f \exists p f (k PathsOn (G) n) p)$
25	21 24	mpbird	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to \forall k \in Vtx (G) \forall n \in Vtx (G) \exists f \exists p f (k PathsOn (G) n) p$
26	6	isconngr	$⊢ G \in W \to (G \in ConnGraph \leftrightarrow \forall k \in Vtx (G) \forall n \in Vtx (G) \exists f \exists p f (k PathsOn (G) n) p)$
27	26	ad2antrl	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to (G \in ConnGraph \leftrightarrow \forall k \in Vtx (G) \forall n \in Vtx (G) \exists f \exists p f (k PathsOn (G) n) p)$
28	25 27	mpbird	$⊢ (N \in V \land (G \in W \land Vtx (G) = \{N\})) \to G \in ConnGraph$
29	28	ex	$⊢ N \in V \to ((G \in W \land Vtx (G) = \{N\}) \to G \in ConnGraph)$
30		snprc	$⊢ \neg N \in V \leftrightarrow \{N\} = \emptyset$
31		eqeq2	$⊢ \{N\} = \emptyset \to (Vtx (G) = \{N\} \leftrightarrow Vtx (G) = \emptyset)$
32	31	anbi2d	$⊢ \{N\} = \emptyset \to ((G \in W \land Vtx (G) = \{N\}) \leftrightarrow (G \in W \land Vtx (G) = \emptyset))$
33		0vconngr	$⊢ (G \in W \land Vtx (G) = \emptyset) \to G \in ConnGraph$
34	32 33	syl6bi	$⊢ \{N\} = \emptyset \to ((G \in W \land Vtx (G) = \{N\}) \to G \in ConnGraph)$
35	30 34	sylbi	$⊢ \neg N \in V \to ((G \in W \land Vtx (G) = \{N\}) \to G \in ConnGraph)$
36	29 35	pm2.61i	$⊢ (G \in W \land Vtx (G) = \{N\}) \to G \in ConnGraph$

Metamath Proof Explorer

Theorem 1conngr

Proof