ushgredgedgloop

Description: In a simple hypergraph there is a 1-1 onto mapping between the indexed edges being loops at a fixed vertex N and the set of loops at this vertex N . (Contributed by AV, 11-Dec-2020) (Revised by AV, 6-Jul-2022)

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

Proof

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

Metamath Proof Explorer

Theorem ushgredgedgloop

Proof