ushgredgedg

Description: In a simple hypergraph there is a 1-1 onto mapping between the indexed edges containing a fixed vertex and the set of edges containing this vertex. (Contributed by AV, 11-Dec-2020)

	Ref	Expression
Hypotheses	ushgredgedg.e	$⊢ E = Edg (G)$
	ushgredgedg.i	$⊢ I = iEdg (G)$
	ushgredgedg.v	$⊢ V = Vtx (G)$
	ushgredgedg.a	$⊢ A = \{i \in dom I \| N \in I (i)\}$
	ushgredgedg.b	$⊢ B = \{e \in E \| N \in e\}$
	ushgredgedg.f	$⊢ F = (x \in A ⟼ I (x))$
Assertion	ushgredgedg	$⊢ (G \in USHGraph \land N \in V) \to F : A \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		ushgredgedg.e	$⊢ E = Edg (G)$
2		ushgredgedg.i	$⊢ I = iEdg (G)$
3		ushgredgedg.v	$⊢ V = Vtx (G)$
4		ushgredgedg.a	$⊢ A = \{i \in dom I \| N \in I (i)\}$
5		ushgredgedg.b	$⊢ B = \{e \in E \| N \in e\}$
6		ushgredgedg.f	$⊢ F = (x \in A ⟼ I (x))$
7		eqid	$⊢ Vtx (G) = Vtx (G)$
8	7 2	ushgrf	$⊢ G \in USHGraph \to I : dom I \underset{1-1}{⟶} 𝒫 Vtx (G) ∖ \{\emptyset\}$
9	8	adantr	$⊢ (G \in USHGraph \land N \in V) \to I : dom I \underset{1-1}{⟶} 𝒫 Vtx (G) ∖ \{\emptyset\}$
10		ssrab2	$⊢ \{i \in dom I \| N \in I (i)\} \subseteq dom I$
11		f1ores	$⊢ (I : dom I \underset{1-1}{⟶} 𝒫 Vtx (G) ∖ \{\emptyset\} \land \{i \in dom I \| N \in I (i)\} \subseteq dom I) \to ({I ↾}_{\{i \in dom I \| N \in I (i)\}}) : \{i \in dom I \| N \in I (i)\} \underset{1-1 onto}{⟶} I [\{i \in dom I \| N \in I (i)\}]$
12	9 10 11	sylancl	$⊢ (G \in USHGraph \land N \in V) \to ({I ↾}_{\{i \in dom I \| N \in I (i)\}}) : \{i \in dom I \| N \in I (i)\} \underset{1-1 onto}{⟶} I [\{i \in dom I \| N \in I (i)\}]$
13	4	a1i	$⊢ (G \in USHGraph \land N \in V) \to A = \{i \in dom I \| N \in I (i)\}$
14		eqidd	$⊢ ((G \in USHGraph \land N \in V) \land x \in A) \to I (x) = I (x)$
15	13 14	mpteq12dva	$⊢ (G \in USHGraph \land N \in V) \to (x \in A ⟼ I (x)) = (x \in \{i \in dom I \| N \in I (i)\} ⟼ I (x))$
16	6 15	eqtrid	$⊢ (G \in USHGraph \land N \in V) \to F = (x \in \{i \in dom I \| N \in I (i)\} ⟼ I (x))$
17		f1f	$⊢ I : dom I \underset{1-1}{⟶} 𝒫 Vtx (G) ∖ \{\emptyset\} \to I : dom I ⟶ 𝒫 Vtx (G) ∖ \{\emptyset\}$
18	8 17	syl	$⊢ G \in USHGraph \to I : dom I ⟶ 𝒫 Vtx (G) ∖ \{\emptyset\}$
19	10	a1i	$⊢ G \in USHGraph \to \{i \in dom I \| N \in I (i)\} \subseteq dom I$
20	18 19	feqresmpt	$⊢ G \in USHGraph \to {I ↾}_{\{i \in dom I \| N \in I (i)\}} = (x \in \{i \in dom I \| N \in I (i)\} ⟼ I (x))$
21	20	adantr	$⊢ (G \in USHGraph \land N \in V) \to {I ↾}_{\{i \in dom I \| N \in I (i)\}} = (x \in \{i \in dom I \| N \in I (i)\} ⟼ I (x))$
22	21	eqcomd	$⊢ (G \in USHGraph \land N \in V) \to (x \in \{i \in dom I \| N \in I (i)\} ⟼ I (x)) = {I ↾}_{\{i \in dom I \| N \in I (i)\}}$
23	16 22	eqtrd	$⊢ (G \in USHGraph \land N \in V) \to F = {I ↾}_{\{i \in dom I \| N \in I (i)\}}$
24		ushgruhgr	$⊢ G \in USHGraph \to G \in UHGraph$
25		eqid	$⊢ iEdg (G) = iEdg (G)$
26	25	uhgrfun	$⊢ G \in UHGraph \to Fun iEdg (G)$
27	24 26	syl	$⊢ G \in USHGraph \to Fun iEdg (G)$
28	2	funeqi	$⊢ Fun I \leftrightarrow Fun iEdg (G)$
29	27 28	sylibr	$⊢ G \in USHGraph \to Fun I$
30	29	adantr	$⊢ (G \in USHGraph \land N \in V) \to Fun I$
31		dfimafn	$⊢ (Fun I \land \{i \in dom I \| N \in I (i)\} \subseteq dom I) \to I [\{i \in dom I \| N \in I (i)\}] = \{e \| \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = e\}$
32	30 10 31	sylancl	$⊢ (G \in USHGraph \land N \in V) \to I [\{i \in dom I \| N \in I (i)\}] = \{e \| \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = e\}$
33		fveq2	$⊢ i = j \to I (i) = I (j)$
34	33	eleq2d	$⊢ i = j \to (N \in I (i) \leftrightarrow N \in I (j))$
35	34	elrab	$⊢ j \in \{i \in dom I \| N \in I (i)\} \leftrightarrow (j \in dom I \land N \in I (j))$
36		simpl	$⊢ (j \in dom I \land N \in I (j)) \to j \in dom I$
37		fvelrn	$⊢ (Fun I \land j \in dom I) \to I (j) \in ran I$
38	2	eqcomi	$⊢ iEdg (G) = I$
39	38	rneqi	$⊢ ran iEdg (G) = ran I$
40	39	eleq2i	$⊢ I (j) \in ran iEdg (G) \leftrightarrow I (j) \in ran I$
41	37 40	sylibr	$⊢ (Fun I \land j \in dom I) \to I (j) \in ran iEdg (G)$
42	30 36 41	syl2an	$⊢ ((G \in USHGraph \land N \in V) \land (j \in dom I \land N \in I (j))) \to I (j) \in ran iEdg (G)$
43	42	3adant3	$⊢ ((G \in USHGraph \land N \in V) \land (j \in dom I \land N \in I (j)) \land I (j) = f) \to I (j) \in ran iEdg (G)$
44		eleq1	$⊢ f = I (j) \to (f \in ran iEdg (G) \leftrightarrow I (j) \in ran iEdg (G))$
45	44	eqcoms	$⊢ I (j) = f \to (f \in ran iEdg (G) \leftrightarrow I (j) \in ran iEdg (G))$
46	45	3ad2ant3	$⊢ ((G \in USHGraph \land N \in V) \land (j \in dom I \land N \in I (j)) \land I (j) = f) \to (f \in ran iEdg (G) \leftrightarrow I (j) \in ran iEdg (G))$
47	43 46	mpbird	$⊢ ((G \in USHGraph \land N \in V) \land (j \in dom I \land N \in I (j)) \land I (j) = f) \to f \in ran iEdg (G)$
48		edgval	$⊢ Edg (G) = ran iEdg (G)$
49	48	a1i	$⊢ G \in USHGraph \to Edg (G) = ran iEdg (G)$
50	1 49	eqtrid	$⊢ G \in USHGraph \to E = ran iEdg (G)$
51	50	eleq2d	$⊢ G \in USHGraph \to (f \in E \leftrightarrow f \in ran iEdg (G))$
52	51	adantr	$⊢ (G \in USHGraph \land N \in V) \to (f \in E \leftrightarrow f \in ran iEdg (G))$
53	52	3ad2ant1	$⊢ ((G \in USHGraph \land N \in V) \land (j \in dom I \land N \in I (j)) \land I (j) = f) \to (f \in E \leftrightarrow f \in ran iEdg (G))$
54	47 53	mpbird	$⊢ ((G \in USHGraph \land N \in V) \land (j \in dom I \land N \in I (j)) \land I (j) = f) \to f \in E$
55		eleq2	$⊢ I (j) = f \to (N \in I (j) \leftrightarrow N \in f)$
56	55	biimpcd	$⊢ N \in I (j) \to (I (j) = f \to N \in f)$
57	56	adantl	$⊢ (j \in dom I \land N \in I (j)) \to (I (j) = f \to N \in f)$
58	57	a1i	$⊢ (G \in USHGraph \land N \in V) \to ((j \in dom I \land N \in I (j)) \to (I (j) = f \to N \in f))$
59	58	3imp	$⊢ ((G \in USHGraph \land N \in V) \land (j \in dom I \land N \in I (j)) \land I (j) = f) \to N \in f$
60	54 59	jca	$⊢ ((G \in USHGraph \land N \in V) \land (j \in dom I \land N \in I (j)) \land I (j) = f) \to (f \in E \land N \in f)$
61	60	3exp	$⊢ (G \in USHGraph \land N \in V) \to ((j \in dom I \land N \in I (j)) \to (I (j) = f \to (f \in E \land N \in f)))$
62	35 61	syl5bi	$⊢ (G \in USHGraph \land N \in V) \to (j \in \{i \in dom I \| N \in I (i)\} \to (I (j) = f \to (f \in E \land N \in f)))$
63	62	rexlimdv	$⊢ (G \in USHGraph \land N \in V) \to (\exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f \to (f \in E \land N \in f))$
64	27	funfnd	$⊢ G \in USHGraph \to iEdg (G) Fn dom iEdg (G)$
65		fvelrnb	$⊢ iEdg (G) Fn dom iEdg (G) \to (f \in ran iEdg (G) \leftrightarrow \exists j \in dom iEdg (G) iEdg (G) (j) = f)$
66	64 65	syl	$⊢ G \in USHGraph \to (f \in ran iEdg (G) \leftrightarrow \exists j \in dom iEdg (G) iEdg (G) (j) = f)$
67	38	dmeqi	$⊢ dom iEdg (G) = dom I$
68	67	eleq2i	$⊢ j \in dom iEdg (G) \leftrightarrow j \in dom I$
69	68	biimpi	$⊢ j \in dom iEdg (G) \to j \in dom I$
70	69	adantr	$⊢ (j \in dom iEdg (G) \land iEdg (G) (j) = f) \to j \in dom I$
71	70	adantl	$⊢ ((G \in USHGraph \land N \in f) \land (j \in dom iEdg (G) \land iEdg (G) (j) = f)) \to j \in dom I$
72	38	fveq1i	$⊢ iEdg (G) (j) = I (j)$
73	72	eqeq2i	$⊢ f = iEdg (G) (j) \leftrightarrow f = I (j)$
74	73	biimpi	$⊢ f = iEdg (G) (j) \to f = I (j)$
75	74	eqcoms	$⊢ iEdg (G) (j) = f \to f = I (j)$
76	75	eleq2d	$⊢ iEdg (G) (j) = f \to (N \in f \leftrightarrow N \in I (j))$
77	76	biimpcd	$⊢ N \in f \to (iEdg (G) (j) = f \to N \in I (j))$
78	77	adantl	$⊢ (G \in USHGraph \land N \in f) \to (iEdg (G) (j) = f \to N \in I (j))$
79	78	adantld	$⊢ (G \in USHGraph \land N \in f) \to ((j \in dom iEdg (G) \land iEdg (G) (j) = f) \to N \in I (j))$
80	79	imp	$⊢ ((G \in USHGraph \land N \in f) \land (j \in dom iEdg (G) \land iEdg (G) (j) = f)) \to N \in I (j)$
81	71 80	jca	$⊢ ((G \in USHGraph \land N \in f) \land (j \in dom iEdg (G) \land iEdg (G) (j) = f)) \to (j \in dom I \land N \in I (j))$
82	81 35	sylibr	$⊢ ((G \in USHGraph \land N \in f) \land (j \in dom iEdg (G) \land iEdg (G) (j) = f)) \to j \in \{i \in dom I \| N \in I (i)\}$
83	72	eqeq1i	$⊢ iEdg (G) (j) = f \leftrightarrow I (j) = f$
84	83	biimpi	$⊢ iEdg (G) (j) = f \to I (j) = f$
85	84	adantl	$⊢ (j \in dom iEdg (G) \land iEdg (G) (j) = f) \to I (j) = f$
86	85	adantl	$⊢ ((G \in USHGraph \land N \in f) \land (j \in dom iEdg (G) \land iEdg (G) (j) = f)) \to I (j) = f$
87	82 86	jca	$⊢ ((G \in USHGraph \land N \in f) \land (j \in dom iEdg (G) \land iEdg (G) (j) = f)) \to (j \in \{i \in dom I \| N \in I (i)\} \land I (j) = f)$
88	87	ex	$⊢ (G \in USHGraph \land N \in f) \to ((j \in dom iEdg (G) \land iEdg (G) (j) = f) \to (j \in \{i \in dom I \| N \in I (i)\} \land I (j) = f))$
89	88	reximdv2	$⊢ (G \in USHGraph \land N \in f) \to (\exists j \in dom iEdg (G) iEdg (G) (j) = f \to \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f)$
90	89	ex	$⊢ G \in USHGraph \to (N \in f \to (\exists j \in dom iEdg (G) iEdg (G) (j) = f \to \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f))$
91	90	com23	$⊢ G \in USHGraph \to (\exists j \in dom iEdg (G) iEdg (G) (j) = f \to (N \in f \to \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f))$
92	66 91	sylbid	$⊢ G \in USHGraph \to (f \in ran iEdg (G) \to (N \in f \to \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f))$
93	51 92	sylbid	$⊢ G \in USHGraph \to (f \in E \to (N \in f \to \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f))$
94	93	impd	$⊢ G \in USHGraph \to ((f \in E \land N \in f) \to \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f)$
95	94	adantr	$⊢ (G \in USHGraph \land N \in V) \to ((f \in E \land N \in f) \to \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f)$
96	63 95	impbid	$⊢ (G \in USHGraph \land N \in V) \to (\exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f \leftrightarrow (f \in E \land N \in f))$
97		vex	$⊢ f \in V$
98		eqeq2	$⊢ e = f \to (I (j) = e \leftrightarrow I (j) = f)$
99	98	rexbidv	$⊢ e = f \to (\exists j \in \{i \in dom I \| N \in I (i)\} I (j) = e \leftrightarrow \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f)$
100	97 99	elab	$⊢ f \in \{e \| \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = e\} \leftrightarrow \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = f$
101		eleq2	$⊢ e = f \to (N \in e \leftrightarrow N \in f)$
102	101 5	elrab2	$⊢ f \in B \leftrightarrow (f \in E \land N \in f)$
103	96 100 102	3bitr4g	$⊢ (G \in USHGraph \land N \in V) \to (f \in \{e \| \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = e\} \leftrightarrow f \in B)$
104	103	eqrdv	$⊢ (G \in USHGraph \land N \in V) \to \{e \| \exists j \in \{i \in dom I \| N \in I (i)\} I (j) = e\} = B$
105	32 104	eqtrd	$⊢ (G \in USHGraph \land N \in V) \to I [\{i \in dom I \| N \in I (i)\}] = B$
106	105	eqcomd	$⊢ (G \in USHGraph \land N \in V) \to B = I [\{i \in dom I \| N \in I (i)\}]$
107	23 13 106	f1oeq123d	$⊢ (G \in USHGraph \land N \in V) \to (F : A \underset{1-1 onto}{⟶} B \leftrightarrow ({I ↾}_{\{i \in dom I \| N \in I (i)\}}) : \{i \in dom I \| N \in I (i)\} \underset{1-1 onto}{⟶} I [\{i \in dom I \| N \in I (i)\}])$
108	12 107	mpbird	$⊢ (G \in USHGraph \land N \in V) \to F : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem ushgredgedg

Proof