usgredg2vlem2

	Ref	Expression
Hypotheses	usgredg2v.v	$⊢ V = Vtx (G)$
	usgredg2v.e	$⊢ E = iEdg (G)$
	usgredg2v.a	$⊢ A = \{x \in dom E \| N \in E (x)\}$
Assertion	usgredg2vlem2	$⊢ (G \in USGraph \land Y \in A) \to (I = (ι z \in V \| E (Y) = \{z, N\}) \to E (Y) = \{I, N\})$

Proof

Step	Hyp	Ref	Expression
1		usgredg2v.v	$⊢ V = Vtx (G)$
2		usgredg2v.e	$⊢ E = iEdg (G)$
3		usgredg2v.a	$⊢ A = \{x \in dom E \| N \in E (x)\}$
4		fveq2	$⊢ x = Y \to E (x) = E (Y)$
5	4	eleq2d	$⊢ x = Y \to (N \in E (x) \leftrightarrow N \in E (Y))$
6	5 3	elrab2	$⊢ Y \in A \leftrightarrow (Y \in dom E \land N \in E (Y))$
7	6	biimpi	$⊢ Y \in A \to (Y \in dom E \land N \in E (Y))$
8	1 2	usgredgreu	$⊢ (G \in USGraph \land Y \in dom E \land N \in E (Y)) \to \exists! z \in V E (Y) = \{N, z\}$
9	8	3expb	$⊢ (G \in USGraph \land (Y \in dom E \land N \in E (Y))) \to \exists! z \in V E (Y) = \{N, z\}$
10	1 2 3	usgredg2vlem1	$⊢ (G \in USGraph \land Y \in A) \to (ι z \in V \| E (Y) = \{z, N\}) \in V$
11	10	adantlr	$⊢ ((G \in USGraph \land (Y \in dom E \land N \in E (Y))) \land Y \in A) \to (ι z \in V \| E (Y) = \{z, N\}) \in V$
12	11	ad4ant23	$⊢ (((\exists! z \in V E (Y) = \{N, z\} \land (G \in USGraph \land (Y \in dom E \land N \in E (Y)))) \land Y \in A) \land I = (ι z \in V \| E (Y) = \{z, N\})) \to (ι z \in V \| E (Y) = \{z, N\}) \in V$
13		eleq1	$⊢ I = (ι z \in V \| E (Y) = \{z, N\}) \to (I \in V \leftrightarrow (ι z \in V \| E (Y) = \{z, N\}) \in V)$
14	13	adantl	$⊢ (((\exists! z \in V E (Y) = \{N, z\} \land (G \in USGraph \land (Y \in dom E \land N \in E (Y)))) \land Y \in A) \land I = (ι z \in V \| E (Y) = \{z, N\})) \to (I \in V \leftrightarrow (ι z \in V \| E (Y) = \{z, N\}) \in V)$
15	12 14	mpbird	$⊢ (((\exists! z \in V E (Y) = \{N, z\} \land (G \in USGraph \land (Y \in dom E \land N \in E (Y)))) \land Y \in A) \land I = (ι z \in V \| E (Y) = \{z, N\})) \to I \in V$
16		prcom	$⊢ \{N, z\} = \{z, N\}$
17	16	eqeq2i	$⊢ E (Y) = \{N, z\} \leftrightarrow E (Y) = \{z, N\}$
18	17	reubii	$⊢ \exists! z \in V E (Y) = \{N, z\} \leftrightarrow \exists! z \in V E (Y) = \{z, N\}$
19	18	biimpi	$⊢ \exists! z \in V E (Y) = \{N, z\} \to \exists! z \in V E (Y) = \{z, N\}$
20	19	ad3antrrr	$⊢ (((\exists! z \in V E (Y) = \{N, z\} \land (G \in USGraph \land (Y \in dom E \land N \in E (Y)))) \land Y \in A) \land I = (ι z \in V \| E (Y) = \{z, N\})) \to \exists! z \in V E (Y) = \{z, N\}$
21		preq1	$⊢ z = I \to \{z, N\} = \{I, N\}$
22	21	eqeq2d	$⊢ z = I \to (E (Y) = \{z, N\} \leftrightarrow E (Y) = \{I, N\})$
23	22	riota2	$⊢ (I \in V \land \exists! z \in V E (Y) = \{z, N\}) \to (E (Y) = \{I, N\} \leftrightarrow (ι z \in V \| E (Y) = \{z, N\}) = I)$
24	15 20 23	syl2anc	$⊢ (((\exists! z \in V E (Y) = \{N, z\} \land (G \in USGraph \land (Y \in dom E \land N \in E (Y)))) \land Y \in A) \land I = (ι z \in V \| E (Y) = \{z, N\})) \to (E (Y) = \{I, N\} \leftrightarrow (ι z \in V \| E (Y) = \{z, N\}) = I)$
25	24	exbiri	$⊢ ((\exists! z \in V E (Y) = \{N, z\} \land (G \in USGraph \land (Y \in dom E \land N \in E (Y)))) \land Y \in A) \to (I = (ι z \in V \| E (Y) = \{z, N\}) \to ((ι z \in V \| E (Y) = \{z, N\}) = I \to E (Y) = \{I, N\}))$
26	25	com13	$⊢ (ι z \in V \| E (Y) = \{z, N\}) = I \to (I = (ι z \in V \| E (Y) = \{z, N\}) \to (((\exists! z \in V E (Y) = \{N, z\} \land (G \in USGraph \land (Y \in dom E \land N \in E (Y)))) \land Y \in A) \to E (Y) = \{I, N\}))$
27	26	eqcoms	$⊢ I = (ι z \in V \| E (Y) = \{z, N\}) \to (I = (ι z \in V \| E (Y) = \{z, N\}) \to (((\exists! z \in V E (Y) = \{N, z\} \land (G \in USGraph \land (Y \in dom E \land N \in E (Y)))) \land Y \in A) \to E (Y) = \{I, N\}))$
28	27	pm2.43i	$⊢ I = (ι z \in V \| E (Y) = \{z, N\}) \to (((\exists! z \in V E (Y) = \{N, z\} \land (G \in USGraph \land (Y \in dom E \land N \in E (Y)))) \land Y \in A) \to E (Y) = \{I, N\})$
29	28	expdcom	$⊢ (\exists! z \in V E (Y) = \{N, z\} \land (G \in USGraph \land (Y \in dom E \land N \in E (Y)))) \to (Y \in A \to (I = (ι z \in V \| E (Y) = \{z, N\}) \to E (Y) = \{I, N\}))$
30	9 29	mpancom	$⊢ (G \in USGraph \land (Y \in dom E \land N \in E (Y))) \to (Y \in A \to (I = (ι z \in V \| E (Y) = \{z, N\}) \to E (Y) = \{I, N\}))$
31	30	expcom	$⊢ (Y \in dom E \land N \in E (Y)) \to (G \in USGraph \to (Y \in A \to (I = (ι z \in V \| E (Y) = \{z, N\}) \to E (Y) = \{I, N\})))$
32	31	com23	$⊢ (Y \in dom E \land N \in E (Y)) \to (Y \in A \to (G \in USGraph \to (I = (ι z \in V \| E (Y) = \{z, N\}) \to E (Y) = \{I, N\})))$
33	7 32	mpcom	$⊢ Y \in A \to (G \in USGraph \to (I = (ι z \in V \| E (Y) = \{z, N\}) \to E (Y) = \{I, N\}))$
34	33	impcom	$⊢ (G \in USGraph \land Y \in A) \to (I = (ι z \in V \| E (Y) = \{z, N\}) \to E (Y) = \{I, N\})$

Metamath Proof Explorer

Theorem usgredg2vlem2

Proof