Theorem ushgredgedgloop 16034

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

Hypotheses

Ref	Expression
ushgredgedgloop.e	⊢ 𝐸 = (Edg‘𝐺)
ushgredgedgloop.i	⊢ 𝐼 = (iEdg‘𝐺)
ushgredgedgloop.a	⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}
ushgredgedgloop.b	⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑒 = {𝑁}}
ushgredgedgloop.f	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥))

Assertion

Ref	Expression
ushgredgedgloop	⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵)

Distinct variable groups:   𝐵,𝑒   𝑒,𝐸,𝑖   𝑒,𝐺,𝑖,𝑥   𝑒,𝐼,𝑖,𝑥   𝑒,𝑁,𝑖,𝑥   𝑒,𝑉,𝑖,𝑥

Allowed substitution hints:   𝐴(𝑥,𝑒,𝑖)   𝐵(𝑥,𝑖)   𝐸(𝑥)   𝐹(𝑥,𝑒,𝑖)

Proof of Theorem ushgredgedgloop

Dummy variables 𝑓 𝑗 𝑝 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2229	. . . . 5 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
2		ushgredgedgloop.i	. . . . 5 ⊢ 𝐼 = (iEdg‘𝐺)
3	1, 2	ushgrfm 15882	. . . 4 ⊢ (𝐺 ∈ USHGraph → 𝐼:dom 𝐼–1-1→{𝑝 ∈ 𝒫 (Vtx‘𝐺) ∣ ∃𝑤 𝑤 ∈ 𝑝})
4	3	adantr 276	. . 3 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐼:dom 𝐼–1-1→{𝑝 ∈ 𝒫 (Vtx‘𝐺) ∣ ∃𝑤 𝑤 ∈ 𝑝})
5		ssrab2 3309	. . 3 ⊢ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ⊆ dom 𝐼
6		f1ores 5589	. . 3 ⊢ ((𝐼:dom 𝐼–1-1→{𝑝 ∈ 𝒫 (Vtx‘𝐺) ∣ ∃𝑤 𝑤 ∈ 𝑝} ∧ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ⊆ dom 𝐼) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}):{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}))
7	4, 5, 6	sylancl 413	. 2 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}):{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}))
8		ushgredgedgloop.f	. . . . 5 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥))
9		ushgredgedgloop.a	. . . . . . 7 ⊢ 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}
10	9	a1i 9	. . . . . 6 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐴 = {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}})
11		eqidd 2230	. . . . . 6 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ 𝑥 ∈ 𝐴) → (𝐼‘𝑥) = (𝐼‘𝑥))
12	10, 11	mpteq12dva 4165	. . . . 5 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝑥 ∈ 𝐴 ↦ (𝐼‘𝑥)) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ↦ (𝐼‘𝑥)))
13	8, 12	eqtrid 2274	. . . 4 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹 = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ↦ (𝐼‘𝑥)))
14		f1f 5533	. . . . . . 7 ⊢ (𝐼:dom 𝐼–1-1→{𝑝 ∈ 𝒫 (Vtx‘𝐺) ∣ ∃𝑤 𝑤 ∈ 𝑝} → 𝐼:dom 𝐼⟶{𝑝 ∈ 𝒫 (Vtx‘𝐺) ∣ ∃𝑤 𝑤 ∈ 𝑝})
15	3, 14	syl 14	. . . . . 6 ⊢ (𝐺 ∈ USHGraph → 𝐼:dom 𝐼⟶{𝑝 ∈ 𝒫 (Vtx‘𝐺) ∣ ∃𝑤 𝑤 ∈ 𝑝})
16	5	a1i 9	. . . . . 6 ⊢ (𝐺 ∈ USHGraph → {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ⊆ dom 𝐼)
17	15, 16	feqresmpt 5690	. . . . 5 ⊢ (𝐺 ∈ USHGraph → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ↦ (𝐼‘𝑥)))
18	17	adantr 276	. . . 4 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}) = (𝑥 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ↦ (𝐼‘𝑥)))
19	13, 18	eqtr4d 2265	. . 3 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹 = (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}))
20		ushgruhgr 15888	. . . . . . . 8 ⊢ (𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph)
21		eqid 2229	. . . . . . . . 9 ⊢ (iEdg‘𝐺) = (iEdg‘𝐺)
22	21	uhgrfun 15885	. . . . . . . 8 ⊢ (𝐺 ∈ UHGraph → Fun (iEdg‘𝐺))
23	20, 22	syl 14	. . . . . . 7 ⊢ (𝐺 ∈ USHGraph → Fun (iEdg‘𝐺))
24	2	funeqi 5339	. . . . . . 7 ⊢ (Fun 𝐼 ↔ Fun (iEdg‘𝐺))
25	23, 24	sylibr 134	. . . . . 6 ⊢ (𝐺 ∈ USHGraph → Fun 𝐼)
26	25	adantr 276	. . . . 5 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → Fun 𝐼)
27		dfimafn 5684	. . . . 5 ⊢ ((Fun 𝐼 ∧ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ⊆ dom 𝐼) → (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}) = {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑒})
28	26, 5, 27	sylancl 413	. . . 4 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}) = {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑒})
29		fveqeq2 5638	. . . . . . . . . 10 ⊢ (𝑖 = 𝑗 → ((𝐼‘𝑖) = {𝑁} ↔ (𝐼‘𝑗) = {𝑁}))
30	29	elrab 2959	. . . . . . . . 9 ⊢ (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ↔ (𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}))
31		simpl 109	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) → 𝑗 ∈ dom 𝐼)
32		fvelrn 5768	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝐼 ∧ 𝑗 ∈ dom 𝐼) → (𝐼‘𝑗) ∈ ran 𝐼)
33	2	eqcomi 2233	. . . . . . . . . . . . . . . . 17 ⊢ (iEdg‘𝐺) = 𝐼
34	33	rneqi 4952	. . . . . . . . . . . . . . . 16 ⊢ ran (iEdg‘𝐺) = ran 𝐼
35	32, 34	eleqtrrdi 2323	. . . . . . . . . . . . . . 15 ⊢ ((Fun 𝐼 ∧ 𝑗 ∈ dom 𝐼) → (𝐼‘𝑗) ∈ ran (iEdg‘𝐺))
36	26, 31, 35	syl2an 289	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁})) → (𝐼‘𝑗) ∈ ran (iEdg‘𝐺))
37	36	3adant3 1041	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) ∧ (𝐼‘𝑗) = 𝑓) → (𝐼‘𝑗) ∈ ran (iEdg‘𝐺))
38		eleq1 2292	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (𝐼‘𝑗) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼‘𝑗) ∈ ran (iEdg‘𝐺)))
39	38	eqcoms 2232	. . . . . . . . . . . . . 14 ⊢ ((𝐼‘𝑗) = 𝑓 → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼‘𝑗) ∈ ran (iEdg‘𝐺)))
40	39	3ad2ant3 1044	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) ∧ (𝐼‘𝑗) = 𝑓) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ (𝐼‘𝑗) ∈ ran (iEdg‘𝐺)))
41	37, 40	mpbird 167	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) ∧ (𝐼‘𝑗) = 𝑓) → 𝑓 ∈ ran (iEdg‘𝐺))
42		ushgredgedgloop.e	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (Edg‘𝐺)
43		edgvalg 15868	. . . . . . . . . . . . . . . 16 ⊢ (𝐺 ∈ USHGraph → (Edg‘𝐺) = ran (iEdg‘𝐺))
44	42, 43	eqtrid 2274	. . . . . . . . . . . . . . 15 ⊢ (𝐺 ∈ USHGraph → 𝐸 = ran (iEdg‘𝐺))
45	44	eleq2d 2299	. . . . . . . . . . . . . 14 ⊢ (𝐺 ∈ USHGraph → (𝑓 ∈ 𝐸 ↔ 𝑓 ∈ ran (iEdg‘𝐺)))
46	45	adantr 276	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝑓 ∈ 𝐸 ↔ 𝑓 ∈ ran (iEdg‘𝐺)))
47	46	3ad2ant1 1042	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) ∧ (𝐼‘𝑗) = 𝑓) → (𝑓 ∈ 𝐸 ↔ 𝑓 ∈ ran (iEdg‘𝐺)))
48	41, 47	mpbird 167	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) ∧ (𝐼‘𝑗) = 𝑓) → 𝑓 ∈ 𝐸)
49		eqeq1 2236	. . . . . . . . . . . . . . 15 ⊢ ((𝐼‘𝑗) = 𝑓 → ((𝐼‘𝑗) = {𝑁} ↔ 𝑓 = {𝑁}))
50	49	biimpcd 159	. . . . . . . . . . . . . 14 ⊢ ((𝐼‘𝑗) = {𝑁} → ((𝐼‘𝑗) = 𝑓 → 𝑓 = {𝑁}))
51	50	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) → ((𝐼‘𝑗) = 𝑓 → 𝑓 = {𝑁}))
52	51	a1i 9	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → ((𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) → ((𝐼‘𝑗) = 𝑓 → 𝑓 = {𝑁})))
53	52	3imp 1217	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) ∧ (𝐼‘𝑗) = 𝑓) → 𝑓 = {𝑁})
54	48, 53	jca 306	. . . . . . . . . 10 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) ∧ (𝐼‘𝑗) = 𝑓) → (𝑓 ∈ 𝐸 ∧ 𝑓 = {𝑁}))
55	54	3exp 1226	. . . . . . . . 9 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → ((𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}) → ((𝐼‘𝑗) = 𝑓 → (𝑓 ∈ 𝐸 ∧ 𝑓 = {𝑁}))))
56	30, 55	biimtrid 152	. . . . . . . 8 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} → ((𝐼‘𝑗) = 𝑓 → (𝑓 ∈ 𝐸 ∧ 𝑓 = {𝑁}))))
57	56	rexlimdv 2647	. . . . . . 7 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓 → (𝑓 ∈ 𝐸 ∧ 𝑓 = {𝑁})))
58	23	funfnd 5349	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USHGraph → (iEdg‘𝐺) Fn dom (iEdg‘𝐺))
59		fvelrnb 5683	. . . . . . . . . . . 12 ⊢ ((iEdg‘𝐺) Fn dom (iEdg‘𝐺) → (𝑓 ∈ ran (iEdg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓))
60	58, 59	syl 14	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USHGraph → (𝑓 ∈ ran (iEdg‘𝐺) ↔ ∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓))
61	33	dmeqi 4924	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ dom (iEdg‘𝐺) = dom 𝐼
62	61	eleq2i 2296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ dom (iEdg‘𝐺) ↔ 𝑗 ∈ dom 𝐼)
63	62	biimpi 120	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 ∈ dom (iEdg‘𝐺) → 𝑗 ∈ dom 𝐼)
64	63	adantr 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → 𝑗 ∈ dom 𝐼)
65	64	adantl 277	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → 𝑗 ∈ dom 𝐼)
66	33	fveq1i 5630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((iEdg‘𝐺)‘𝑗) = (𝐼‘𝑗)
67	66	eqeq2i 2240	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = ((iEdg‘𝐺)‘𝑗) ↔ 𝑓 = (𝐼‘𝑗))
68	67	biimpi 120	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = ((iEdg‘𝐺)‘𝑗) → 𝑓 = (𝐼‘𝑗))
69	68	eqcoms 2232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((iEdg‘𝐺)‘𝑗) = 𝑓 → 𝑓 = (𝐼‘𝑗))
70	69	eqeq1d 2238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝑓 = {𝑁} ↔ (𝐼‘𝑗) = {𝑁}))
71	70	biimpcd 159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = {𝑁} → (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝐼‘𝑗) = {𝑁}))
72	71	adantl 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝐼‘𝑗) = {𝑁}))
73	72	adantld 278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝐼‘𝑗) = {𝑁}))
74	73	imp 124	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝐼‘𝑗) = {𝑁})
75	65, 74	jca 306	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝑗 ∈ dom 𝐼 ∧ (𝐼‘𝑗) = {𝑁}))
76	75, 30	sylibr 134	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → 𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}})
77	66	eqeq1i 2237	. . . . . . . . . . . . . . . . . . 19 ⊢ (((iEdg‘𝐺)‘𝑗) = 𝑓 ↔ (𝐼‘𝑗) = 𝑓)
78	77	biimpi 120	. . . . . . . . . . . . . . . . . 18 ⊢ (((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝐼‘𝑗) = 𝑓)
79	78	adantl 277	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝐼‘𝑗) = 𝑓)
80	79	adantl 277	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝐼‘𝑗) = 𝑓)
81	76, 80	jca 306	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) ∧ (𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓)) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ∧ (𝐼‘𝑗) = 𝑓))
82	81	ex 115	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → ((𝑗 ∈ dom (iEdg‘𝐺) ∧ ((iEdg‘𝐺)‘𝑗) = 𝑓) → (𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} ∧ (𝐼‘𝑗) = 𝑓)))
83	82	reximdv2 2629	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑓 = {𝑁}) → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓))
84	83	ex 115	. . . . . . . . . . . 12 ⊢ (𝐺 ∈ USHGraph → (𝑓 = {𝑁} → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓)))
85	84	com23 78	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USHGraph → (∃𝑗 ∈ dom (iEdg‘𝐺)((iEdg‘𝐺)‘𝑗) = 𝑓 → (𝑓 = {𝑁} → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓)))
86	60, 85	sylbid 150	. . . . . . . . . 10 ⊢ (𝐺 ∈ USHGraph → (𝑓 ∈ ran (iEdg‘𝐺) → (𝑓 = {𝑁} → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓)))
87	45, 86	sylbid 150	. . . . . . . . 9 ⊢ (𝐺 ∈ USHGraph → (𝑓 ∈ 𝐸 → (𝑓 = {𝑁} → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓)))
88	87	impd 254	. . . . . . . 8 ⊢ (𝐺 ∈ USHGraph → ((𝑓 ∈ 𝐸 ∧ 𝑓 = {𝑁}) → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓))
89	88	adantr 276	. . . . . . 7 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → ((𝑓 ∈ 𝐸 ∧ 𝑓 = {𝑁}) → ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓))
90	57, 89	impbid 129	. . . . . 6 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓 ↔ (𝑓 ∈ 𝐸 ∧ 𝑓 = {𝑁})))
91		vex 2802	. . . . . . 7 ⊢ 𝑓 ∈ V
92		eqeq2 2239	. . . . . . . 8 ⊢ (𝑒 = 𝑓 → ((𝐼‘𝑗) = 𝑒 ↔ (𝐼‘𝑗) = 𝑓))
93	92	rexbidv 2531	. . . . . . 7 ⊢ (𝑒 = 𝑓 → (∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑒 ↔ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓))
94	91, 93	elab 2947	. . . . . 6 ⊢ (𝑓 ∈ {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑒} ↔ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑓)
95		eqeq1 2236	. . . . . . 7 ⊢ (𝑒 = 𝑓 → (𝑒 = {𝑁} ↔ 𝑓 = {𝑁}))
96		ushgredgedgloop.b	. . . . . . 7 ⊢ 𝐵 = {𝑒 ∈ 𝐸 ∣ 𝑒 = {𝑁}}
97	95, 96	elrab2 2962	. . . . . 6 ⊢ (𝑓 ∈ 𝐵 ↔ (𝑓 ∈ 𝐸 ∧ 𝑓 = {𝑁}))
98	90, 94, 97	3bitr4g 223	. . . . 5 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝑓 ∈ {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑒} ↔ 𝑓 ∈ 𝐵))
99	98	eqrdv 2227	. . . 4 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → {𝑒 ∣ ∃𝑗 ∈ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}} (𝐼‘𝑗) = 𝑒} = 𝐵)
100	28, 99	eqtr2d 2263	. . 3 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐵 = (𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}))
101	19, 10, 100	f1oeq123d 5568	. 2 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐼 ↾ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}):{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}}–1-1-onto→(𝐼 “ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑁}})))
102	7, 101	mpbird 167	1 ⊢ ((𝐺 ∈ USHGraph ∧ 𝑁 ∈ 𝑉) → 𝐹:𝐴–1-1-onto→𝐵)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 1002   = wceq 1395  ∃wex 1538   ∈ wcel 2200  {cab 2215  ∃wrex 2509  {crab 2512   ⊆ wss 3197  𝒫 cpw 3649  {csn 3666   ↦ cmpt 4145  dom cdm 4719  ran crn 4720   ↾ cres 4721   “ cima 4722  Fun wfun 5312   Fn wfn 5313  ⟶wf 5314  –1-1→wf1 5315  –1-1-onto→wf1o 5317  ‘cfv 5318  Vtxcvtx 15821  iEdgciedg 15822  Edgcedg 15866  UHGraphcuhgr 15875  USHGraphcushgr 15876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8098  ax-resscn 8099  ax-1cn 8100  ax-1re 8101  ax-icn 8102  ax-addcl 8103  ax-addrcl 8104  ax-mulcl 8105  ax-addcom 8107  ax-mulcom 8108  ax-addass 8109  ax-mulass 8110  ax-distr 8111  ax-i2m1 8112  ax-1rid 8114  ax-0id 8115  ax-rnegex 8116  ax-cnre 8118

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-csb 3125  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-if 3603  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-mpt 4147  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-rn 4730  df-res 4731  df-ima 4732  df-iota 5278  df-fun 5320  df-fn 5321  df-f 5322  df-f1 5323  df-fo 5324  df-f1o 5325  df-fv 5326  df-riota 5960  df-ov 6010  df-oprab 6011  df-mpo 6012  df-1st 6292  df-2nd 6293  df-sub 8327  df-inn 9119  df-2 9177  df-3 9178  df-4 9179  df-5 9180  df-6 9181  df-7 9182  df-8 9183  df-9 9184  df-n0 9378  df-dec 9587  df-ndx 13043  df-slot 13044  df-base 13046  df-edgf 15814  df-vtx 15823  df-iedg 15824  df-edg 15867  df-uhgrm 15877  df-ushgrm 15878

This theorem is referenced by: (None)