cusgredg

Description: In a complete simple graph, the edges are all the pairs of different vertices. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 1-Nov-2020)

	Ref	Expression
Hypotheses	iscusgrvtx.v	$⊢ V = Vtx (G)$
	iscusgredg.v	$⊢ E = Edg (G)$
Assertion	cusgredg	$⊢ G \in ComplUSGraph \to E = \{x \in 𝒫 V \| \|x\| = 2\}$

Proof

Step	Hyp	Ref	Expression
1		iscusgrvtx.v	$⊢ V = Vtx (G)$
2		iscusgredg.v	$⊢ E = Edg (G)$
3	1 2	iscusgredg	$⊢ G \in ComplUSGraph \leftrightarrow (G \in USGraph \land \forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E)$
4		usgredgss	$⊢ G \in USGraph \to Edg (G) \subseteq \{x \in 𝒫 Vtx (G) \| \|x\| = 2\}$
5	1	pweqi	$⊢ 𝒫 V = 𝒫 Vtx (G)$
6	5	rabeqi	$⊢ \{x \in 𝒫 V \| \|x\| = 2\} = \{x \in 𝒫 Vtx (G) \| \|x\| = 2\}$
7	4 2 6	3sstr4g	$⊢ G \in USGraph \to E \subseteq \{x \in 𝒫 V \| \|x\| = 2\}$
8	7	adantr	$⊢ (G \in USGraph \land \forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E) \to E \subseteq \{x \in 𝒫 V \| \|x\| = 2\}$
9		elss2prb	$⊢ p \in \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow \exists y \in V \exists z \in V (y \neq z \land p = \{y, z\})$
10		sneq	$⊢ v = y \to \{v\} = \{y\}$
11	10	difeq2d	$⊢ v = y \to V ∖ \{v\} = V ∖ \{y\}$
12		preq2	$⊢ v = y \to \{n, v\} = \{n, y\}$
13	12	eleq1d	$⊢ v = y \to (\{n, v\} \in E \leftrightarrow \{n, y\} \in E)$
14	11 13	raleqbidv	$⊢ v = y \to (\forall n \in (V ∖ \{v\}) \{n, v\} \in E \leftrightarrow \forall n \in (V ∖ \{y\}) \{n, y\} \in E)$
15	14	rspcv	$⊢ y \in V \to (\forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E \to \forall n \in (V ∖ \{y\}) \{n, y\} \in E)$
16	15	adantr	$⊢ (y \in V \land z \in V) \to (\forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E \to \forall n \in (V ∖ \{y\}) \{n, y\} \in E)$
17	16	adantr	$⊢ ((y \in V \land z \in V) \land (y \neq z \land p = \{y, z\})) \to (\forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E \to \forall n \in (V ∖ \{y\}) \{n, y\} \in E)$
18		simpr	$⊢ (y \in V \land z \in V) \to z \in V$
19		necom	$⊢ y \neq z \leftrightarrow z \neq y$
20	19	biimpi	$⊢ y \neq z \to z \neq y$
21	20	adantr	$⊢ (y \neq z \land p = \{y, z\}) \to z \neq y$
22	18 21	anim12i	$⊢ ((y \in V \land z \in V) \land (y \neq z \land p = \{y, z\})) \to (z \in V \land z \neq y)$
23		eldifsn	$⊢ z \in (V ∖ \{y\}) \leftrightarrow (z \in V \land z \neq y)$
24	22 23	sylibr	$⊢ ((y \in V \land z \in V) \land (y \neq z \land p = \{y, z\})) \to z \in (V ∖ \{y\})$
25		preq1	$⊢ n = z \to \{n, y\} = \{z, y\}$
26	25	eleq1d	$⊢ n = z \to (\{n, y\} \in E \leftrightarrow \{z, y\} \in E)$
27	26	rspcv	$⊢ z \in (V ∖ \{y\}) \to (\forall n \in (V ∖ \{y\}) \{n, y\} \in E \to \{z, y\} \in E)$
28	24 27	syl	$⊢ ((y \in V \land z \in V) \land (y \neq z \land p = \{y, z\})) \to (\forall n \in (V ∖ \{y\}) \{n, y\} \in E \to \{z, y\} \in E)$
29		id	$⊢ p = \{y, z\} \to p = \{y, z\}$
30		prcom	$⊢ \{y, z\} = \{z, y\}$
31	29 30	eqtr2di	$⊢ p = \{y, z\} \to \{z, y\} = p$
32	31	eleq1d	$⊢ p = \{y, z\} \to (\{z, y\} \in E \leftrightarrow p \in E)$
33	32	biimpd	$⊢ p = \{y, z\} \to (\{z, y\} \in E \to p \in E)$
34	33	a1d	$⊢ p = \{y, z\} \to (G \in USGraph \to (\{z, y\} \in E \to p \in E))$
35	34	ad2antll	$⊢ ((y \in V \land z \in V) \land (y \neq z \land p = \{y, z\})) \to (G \in USGraph \to (\{z, y\} \in E \to p \in E))$
36	35	com23	$⊢ ((y \in V \land z \in V) \land (y \neq z \land p = \{y, z\})) \to (\{z, y\} \in E \to (G \in USGraph \to p \in E))$
37	17 28 36	3syld	$⊢ ((y \in V \land z \in V) \land (y \neq z \land p = \{y, z\})) \to (\forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E \to (G \in USGraph \to p \in E))$
38	37	ex	$⊢ (y \in V \land z \in V) \to ((y \neq z \land p = \{y, z\}) \to (\forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E \to (G \in USGraph \to p \in E)))$
39	38	rexlimivv	$⊢ \exists y \in V \exists z \in V (y \neq z \land p = \{y, z\}) \to (\forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E \to (G \in USGraph \to p \in E))$
40	39	com13	$⊢ G \in USGraph \to (\forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E \to (\exists y \in V \exists z \in V (y \neq z \land p = \{y, z\}) \to p \in E))$
41	40	imp	$⊢ (G \in USGraph \land \forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E) \to (\exists y \in V \exists z \in V (y \neq z \land p = \{y, z\}) \to p \in E)$
42	9 41	biimtrid	$⊢ (G \in USGraph \land \forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E) \to (p \in \{x \in 𝒫 V \| \|x\| = 2\} \to p \in E)$
43	42	ssrdv	$⊢ (G \in USGraph \land \forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E) \to \{x \in 𝒫 V \| \|x\| = 2\} \subseteq E$
44	8 43	eqssd	$⊢ (G \in USGraph \land \forall v \in V \forall n \in (V ∖ \{v\}) \{n, v\} \in E) \to E = \{x \in 𝒫 V \| \|x\| = 2\}$
45	3 44	sylbi	$⊢ G \in ComplUSGraph \to E = \{x \in 𝒫 V \| \|x\| = 2\}$

Metamath Proof Explorer

Theorem cusgredg

Proof