uhgr2edg

Description: If a vertex is adjacent to two different vertices in a hypergraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 11-Feb-2021)

	Ref	Expression
Hypotheses	usgrf1oedg.i	$⊢ I = iEdg (G)$
	usgrf1oedg.e	$⊢ E = Edg (G)$
	uhgr2edg.v	$⊢ V = Vtx (G)$
Assertion	uhgr2edg	$⊢ ((G \in UHGraph \land A \neq B) \land (A \in V \land B \in V \land N \in V) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to \exists x \in dom I \exists y \in dom I (x \neq y \land N \in I (x) \land N \in I (y))$

Proof

Step	Hyp	Ref	Expression
1		usgrf1oedg.i	$⊢ I = iEdg (G)$
2		usgrf1oedg.e	$⊢ E = Edg (G)$
3		uhgr2edg.v	$⊢ V = Vtx (G)$
4		simp1l	$⊢ ((G \in UHGraph \land A \neq B) \land (A \in V \land B \in V \land N \in V) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to G \in UHGraph$
5		simp1r	$⊢ ((G \in UHGraph \land A \neq B) \land (A \in V \land B \in V \land N \in V) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to A \neq B$
6		simp23	$⊢ ((G \in UHGraph \land A \neq B) \land (A \in V \land B \in V \land N \in V) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to N \in V$
7		simp21	$⊢ ((G \in UHGraph \land A \neq B) \land (A \in V \land B \in V \land N \in V) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to A \in V$
8		3simpc	$⊢ (A \in V \land B \in V \land N \in V) \to (B \in V \land N \in V)$
9	8	3ad2ant2	$⊢ ((G \in UHGraph \land A \neq B) \land (A \in V \land B \in V \land N \in V) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to (B \in V \land N \in V)$
10	6 7 9	jca31	$⊢ ((G \in UHGraph \land A \neq B) \land (A \in V \land B \in V \land N \in V) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to ((N \in V \land A \in V) \land (B \in V \land N \in V))$
11	4 5 10	jca31	$⊢ ((G \in UHGraph \land A \neq B) \land (A \in V \land B \in V \land N \in V) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to ((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V)))$
12		simp3	$⊢ ((G \in UHGraph \land A \neq B) \land (A \in V \land B \in V \land N \in V) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to (\{N, A\} \in E \land \{B, N\} \in E)$
13	2	a1i	$⊢ G \in UHGraph \to E = Edg (G)$
14		edgval	$⊢ Edg (G) = ran iEdg (G)$
15	14	a1i	$⊢ G \in UHGraph \to Edg (G) = ran iEdg (G)$
16	1	eqcomi	$⊢ iEdg (G) = I$
17	16	a1i	$⊢ G \in UHGraph \to iEdg (G) = I$
18	17	rneqd	$⊢ G \in UHGraph \to ran iEdg (G) = ran I$
19	13 15 18	3eqtrd	$⊢ G \in UHGraph \to E = ran I$
20	19	eleq2d	$⊢ G \in UHGraph \to (\{N, A\} \in E \leftrightarrow \{N, A\} \in ran I)$
21	19	eleq2d	$⊢ G \in UHGraph \to (\{B, N\} \in E \leftrightarrow \{B, N\} \in ran I)$
22	20 21	anbi12d	$⊢ G \in UHGraph \to ((\{N, A\} \in E \land \{B, N\} \in E) \leftrightarrow (\{N, A\} \in ran I \land \{B, N\} \in ran I))$
23	1	uhgrfun	$⊢ G \in UHGraph \to Fun I$
24	23	funfnd	$⊢ G \in UHGraph \to I Fn dom I$
25		fvelrnb	$⊢ I Fn dom I \to (\{N, A\} \in ran I \leftrightarrow \exists x \in dom I I (x) = \{N, A\})$
26		fvelrnb	$⊢ I Fn dom I \to (\{B, N\} \in ran I \leftrightarrow \exists y \in dom I I (y) = \{B, N\})$
27	25 26	anbi12d	$⊢ I Fn dom I \to ((\{N, A\} \in ran I \land \{B, N\} \in ran I) \leftrightarrow (\exists x \in dom I I (x) = \{N, A\} \land \exists y \in dom I I (y) = \{B, N\}))$
28	24 27	syl	$⊢ G \in UHGraph \to ((\{N, A\} \in ran I \land \{B, N\} \in ran I) \leftrightarrow (\exists x \in dom I I (x) = \{N, A\} \land \exists y \in dom I I (y) = \{B, N\}))$
29	22 28	bitrd	$⊢ G \in UHGraph \to ((\{N, A\} \in E \land \{B, N\} \in E) \leftrightarrow (\exists x \in dom I I (x) = \{N, A\} \land \exists y \in dom I I (y) = \{B, N\}))$
30	29	ad2antrr	$⊢ ((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to ((\{N, A\} \in E \land \{B, N\} \in E) \leftrightarrow (\exists x \in dom I I (x) = \{N, A\} \land \exists y \in dom I I (y) = \{B, N\}))$
31		reeanv	$⊢ \exists x \in dom I \exists y \in dom I (I (x) = \{N, A\} \land I (y) = \{B, N\}) \leftrightarrow (\exists x \in dom I I (x) = \{N, A\} \land \exists y \in dom I I (y) = \{B, N\})$
32		fveqeq2	$⊢ x = y \to (I (x) = \{N, A\} \leftrightarrow I (y) = \{N, A\})$
33	32	anbi1d	$⊢ x = y \to ((I (x) = \{N, A\} \land I (y) = \{B, N\}) \leftrightarrow (I (y) = \{N, A\} \land I (y) = \{B, N\}))$
34		eqtr2	$⊢ (I (y) = \{N, A\} \land I (y) = \{B, N\}) \to \{N, A\} = \{B, N\}$
35		prcom	$⊢ \{B, N\} = \{N, B\}$
36	35	eqeq2i	$⊢ \{N, A\} = \{B, N\} \leftrightarrow \{N, A\} = \{N, B\}$
37		preq12bg	$⊢ ((N \in V \land A \in V) \land (N \in V \land B \in V)) \to (\{N, A\} = \{N, B\} \leftrightarrow ((N = N \land A = B) \lor (N = B \land A = N)))$
38	37	ancom2s	$⊢ ((N \in V \land A \in V) \land (B \in V \land N \in V)) \to (\{N, A\} = \{N, B\} \leftrightarrow ((N = N \land A = B) \lor (N = B \land A = N)))$
39		eqneqall	$⊢ A = B \to (A \neq B \to x \neq y)$
40	39	adantl	$⊢ (N = N \land A = B) \to (A \neq B \to x \neq y)$
41		eqtr	$⊢ (A = N \land N = B) \to A = B$
42	41	ancoms	$⊢ (N = B \land A = N) \to A = B$
43	42 39	syl	$⊢ (N = B \land A = N) \to (A \neq B \to x \neq y)$
44	40 43	jaoi	$⊢ ((N = N \land A = B) \lor (N = B \land A = N)) \to (A \neq B \to x \neq y)$
45	44	adantld	$⊢ ((N = N \land A = B) \lor (N = B \land A = N)) \to ((G \in UHGraph \land A \neq B) \to x \neq y)$
46	38 45	syl6bi	$⊢ ((N \in V \land A \in V) \land (B \in V \land N \in V)) \to (\{N, A\} = \{N, B\} \to ((G \in UHGraph \land A \neq B) \to x \neq y))$
47	46	com3l	$⊢ \{N, A\} = \{N, B\} \to ((G \in UHGraph \land A \neq B) \to (((N \in V \land A \in V) \land (B \in V \land N \in V)) \to x \neq y))$
48	47	impd	$⊢ \{N, A\} = \{N, B\} \to (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to x \neq y)$
49	36 48	sylbi	$⊢ \{N, A\} = \{B, N\} \to (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to x \neq y)$
50	34 49	syl	$⊢ (I (y) = \{N, A\} \land I (y) = \{B, N\}) \to (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to x \neq y)$
51	33 50	syl6bi	$⊢ x = y \to ((I (x) = \{N, A\} \land I (y) = \{B, N\}) \to (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to x \neq y))$
52	51	impcomd	$⊢ x = y \to ((((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \land (I (x) = \{N, A\} \land I (y) = \{B, N\})) \to x \neq y)$
53		ax-1	$⊢ x \neq y \to ((((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \land (I (x) = \{N, A\} \land I (y) = \{B, N\})) \to x \neq y)$
54	52 53	pm2.61ine	$⊢ (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \land (I (x) = \{N, A\} \land I (y) = \{B, N\})) \to x \neq y$
55		prid1g	$⊢ N \in V \to N \in \{N, A\}$
56	55	ad2antrr	$⊢ ((N \in V \land A \in V) \land (B \in V \land N \in V)) \to N \in \{N, A\}$
57	56	adantl	$⊢ ((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to N \in \{N, A\}$
58		eleq2	$⊢ I (x) = \{N, A\} \to (N \in I (x) \leftrightarrow N \in \{N, A\})$
59	57 58	syl5ibr	$⊢ I (x) = \{N, A\} \to (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to N \in I (x))$
60	59	adantr	$⊢ (I (x) = \{N, A\} \land I (y) = \{B, N\}) \to (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to N \in I (x))$
61	60	impcom	$⊢ (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \land (I (x) = \{N, A\} \land I (y) = \{B, N\})) \to N \in I (x)$
62		prid2g	$⊢ N \in V \to N \in \{B, N\}$
63	62	ad2antrr	$⊢ ((N \in V \land A \in V) \land (B \in V \land N \in V)) \to N \in \{B, N\}$
64	63	adantl	$⊢ ((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to N \in \{B, N\}$
65		eleq2	$⊢ I (y) = \{B, N\} \to (N \in I (y) \leftrightarrow N \in \{B, N\})$
66	64 65	syl5ibr	$⊢ I (y) = \{B, N\} \to (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to N \in I (y))$
67	66	adantl	$⊢ (I (x) = \{N, A\} \land I (y) = \{B, N\}) \to (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to N \in I (y))$
68	67	impcom	$⊢ (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \land (I (x) = \{N, A\} \land I (y) = \{B, N\})) \to N \in I (y)$
69	54 61 68	3jca	$⊢ (((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \land (I (x) = \{N, A\} \land I (y) = \{B, N\})) \to (x \neq y \land N \in I (x) \land N \in I (y))$
70	69	ex	$⊢ ((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to ((I (x) = \{N, A\} \land I (y) = \{B, N\}) \to (x \neq y \land N \in I (x) \land N \in I (y)))$
71	70	reximdv	$⊢ ((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to (\exists y \in dom I (I (x) = \{N, A\} \land I (y) = \{B, N\}) \to \exists y \in dom I (x \neq y \land N \in I (x) \land N \in I (y)))$
72	71	reximdv	$⊢ ((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to (\exists x \in dom I \exists y \in dom I (I (x) = \{N, A\} \land I (y) = \{B, N\}) \to \exists x \in dom I \exists y \in dom I (x \neq y \land N \in I (x) \land N \in I (y)))$
73	31 72	syl5bir	$⊢ ((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to ((\exists x \in dom I I (x) = \{N, A\} \land \exists y \in dom I I (y) = \{B, N\}) \to \exists x \in dom I \exists y \in dom I (x \neq y \land N \in I (x) \land N \in I (y)))$
74	30 73	sylbid	$⊢ ((G \in UHGraph \land A \neq B) \land ((N \in V \land A \in V) \land (B \in V \land N \in V))) \to ((\{N, A\} \in E \land \{B, N\} \in E) \to \exists x \in dom I \exists y \in dom I (x \neq y \land N \in I (x) \land N \in I (y)))$
75	11 12 74	sylc	$⊢ ((G \in UHGraph \land A \neq B) \land (A \in V \land B \in V \land N \in V) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to \exists x \in dom I \exists y \in dom I (x \neq y \land N \in I (x) \land N \in I (y))$

Metamath Proof Explorer

Theorem uhgr2edg

Proof