usgredg4

Description: For a vertex incident to an edge there is another vertex incident to the edge. (Contributed by Alexander van der Vekens, 18-Dec-2017) (Revised by AV, 17-Oct-2020)

	Ref	Expression
Hypotheses	usgredg3.v	$⊢ V = Vtx (G)$
	usgredg3.e	$⊢ E = iEdg (G)$
Assertion	usgredg4	$⊢ (G \in USGraph \land X \in dom E \land Y \in E (X)) \to \exists y \in V E (X) = \{Y, y\}$

Proof

Step	Hyp	Ref	Expression
1		usgredg3.v	$⊢ V = Vtx (G)$
2		usgredg3.e	$⊢ E = iEdg (G)$
3	1 2	usgredg3	$⊢ (G \in USGraph \land X \in dom E) \to \exists x \in V \exists z \in V (x \neq z \land E (X) = \{x, z\})$
4		eleq2	$⊢ E (X) = \{x, z\} \to (Y \in E (X) \leftrightarrow Y \in \{x, z\})$
5	4	adantl	$⊢ (x \neq z \land E (X) = \{x, z\}) \to (Y \in E (X) \leftrightarrow Y \in \{x, z\})$
6	5	adantl	$⊢ (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\})) \to (Y \in E (X) \leftrightarrow Y \in \{x, z\})$
7		simplrr	$⊢ (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\})) \to z \in V$
8	7	adantl	$⊢ (Y = x \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to z \in V$
9		preq2	$⊢ y = z \to \{x, y\} = \{x, z\}$
10	9	eqeq2d	$⊢ y = z \to (\{x, z\} = \{x, y\} \leftrightarrow \{x, z\} = \{x, z\})$
11	10	adantl	$⊢ ((Y = x \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \land y = z) \to (\{x, z\} = \{x, y\} \leftrightarrow \{x, z\} = \{x, z\})$
12		eqidd	$⊢ (Y = x \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to \{x, z\} = \{x, z\}$
13	8 11 12	rspcedvd	$⊢ (Y = x \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to \exists y \in V \{x, z\} = \{x, y\}$
14		simprr	$⊢ (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\})) \to E (X) = \{x, z\}$
15		preq1	$⊢ Y = x \to \{Y, y\} = \{x, y\}$
16	14 15	eqeqan12rd	$⊢ (Y = x \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to (E (X) = \{Y, y\} \leftrightarrow \{x, z\} = \{x, y\})$
17	16	rexbidv	$⊢ (Y = x \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to (\exists y \in V E (X) = \{Y, y\} \leftrightarrow \exists y \in V \{x, z\} = \{x, y\})$
18	13 17	mpbird	$⊢ (Y = x \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to \exists y \in V E (X) = \{Y, y\}$
19	18	ex	$⊢ Y = x \to ((((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\})) \to \exists y \in V E (X) = \{Y, y\})$
20		simplrl	$⊢ (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\})) \to x \in V$
21	20	adantl	$⊢ (Y = z \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to x \in V$
22		preq2	$⊢ y = x \to \{z, y\} = \{z, x\}$
23	22	eqeq2d	$⊢ y = x \to (\{x, z\} = \{z, y\} \leftrightarrow \{x, z\} = \{z, x\})$
24	23	adantl	$⊢ ((Y = z \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \land y = x) \to (\{x, z\} = \{z, y\} \leftrightarrow \{x, z\} = \{z, x\})$
25		prcom	$⊢ \{x, z\} = \{z, x\}$
26	25	a1i	$⊢ (Y = z \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to \{x, z\} = \{z, x\}$
27	21 24 26	rspcedvd	$⊢ (Y = z \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to \exists y \in V \{x, z\} = \{z, y\}$
28		preq1	$⊢ Y = z \to \{Y, y\} = \{z, y\}$
29	14 28	eqeqan12rd	$⊢ (Y = z \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to (E (X) = \{Y, y\} \leftrightarrow \{x, z\} = \{z, y\})$
30	29	rexbidv	$⊢ (Y = z \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to (\exists y \in V E (X) = \{Y, y\} \leftrightarrow \exists y \in V \{x, z\} = \{z, y\})$
31	27 30	mpbird	$⊢ (Y = z \land (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\}))) \to \exists y \in V E (X) = \{Y, y\}$
32	31	ex	$⊢ Y = z \to ((((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\})) \to \exists y \in V E (X) = \{Y, y\})$
33	19 32	jaoi	$⊢ (Y = x \lor Y = z) \to ((((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\})) \to \exists y \in V E (X) = \{Y, y\})$
34		elpri	$⊢ Y \in \{x, z\} \to (Y = x \lor Y = z)$
35	33 34	syl11	$⊢ (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\})) \to (Y \in \{x, z\} \to \exists y \in V E (X) = \{Y, y\})$
36	6 35	sylbid	$⊢ (((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \land (x \neq z \land E (X) = \{x, z\})) \to (Y \in E (X) \to \exists y \in V E (X) = \{Y, y\})$
37	36	ex	$⊢ ((G \in USGraph \land X \in dom E) \land (x \in V \land z \in V)) \to ((x \neq z \land E (X) = \{x, z\}) \to (Y \in E (X) \to \exists y \in V E (X) = \{Y, y\}))$
38	37	rexlimdvva	$⊢ (G \in USGraph \land X \in dom E) \to (\exists x \in V \exists z \in V (x \neq z \land E (X) = \{x, z\}) \to (Y \in E (X) \to \exists y \in V E (X) = \{Y, y\}))$
39	3 38	mpd	$⊢ (G \in USGraph \land X \in dom E) \to (Y \in E (X) \to \exists y \in V E (X) = \{Y, y\})$
40	39	3impia	$⊢ (G \in USGraph \land X \in dom E \land Y \in E (X)) \to \exists y \in V E (X) = \{Y, y\}$

Metamath Proof Explorer

Theorem usgredg4

Proof