gricushgr - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > gricushgr		Structured version Visualization version GIF version

Theorem gricushgr 47770

Description: The "is isomorphic to" relation for two simple hypergraphs. (Contributed by AV, 28-Nov-2022.)

**Hypotheses**
Ref	Expression
gricushgr.v	⊢ 𝑉 = (Vtx‘𝐴)
gricushgr.w	⊢ 𝑊 = (Vtx‘𝐵)
gricushgr.e	⊢ 𝐸 = (Edg‘𝐴)
gricushgr.k	⊢ 𝐾 = (Edg‘𝐵)

**Assertion**
Ref	Expression
gricushgr	⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 ≃_𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))

Distinct variable groups: 𝐴,𝑒,𝑓,𝑔 𝐵,𝑒,𝑓,𝑔 𝑒,𝐸,𝑔 𝑔,𝐾 𝑒,𝑉,𝑔 𝑒,𝑊,𝑔 Allowed substitution hints: 𝐸(𝑓) 𝐾(𝑒,𝑓) 𝑉(𝑓) 𝑊(𝑓)

Proof of Theorem gricushgr Dummy variables ℎ 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		gricushgr.v	. . 3 ⊢ 𝑉 = (Vtx‘𝐴)
2		gricushgr.w	. . 3 ⊢ 𝑊 = (Vtx‘𝐵)
3		eqid 2740	. . 3 ⊢ (iEdg‘𝐴) = (iEdg‘𝐴)
4		eqid 2740	. . 3 ⊢ (iEdg‘𝐵) = (iEdg‘𝐵)
5	1, 2, 3, 4	dfgric2 47768	. 2 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 ≃_𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))))))
6		fvex 6933	. . . . . . . . . 10 ⊢ (iEdg‘𝐵) ∈ V
7		vex 3492	. . . . . . . . . . 11 ⊢ ℎ ∈ V
8		fvex 6933	. . . . . . . . . . . 12 ⊢ (iEdg‘𝐴) ∈ V
9	8	cnvex 7965	. . . . . . . . . . 11 ⊢ ^◡(iEdg‘𝐴) ∈ V
10	7, 9	coex 7970	. . . . . . . . . 10 ⊢ (ℎ ∘ ^◡(iEdg‘𝐴)) ∈ V
11	6, 10	coex 7970	. . . . . . . . 9 ⊢ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) ∈ V
12	11	a1i 11	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) ∈ V)
13	2, 4	ushgrf 29098	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1→(𝒫 𝑊 ∖ {∅}))
14		f1f1orn 6873	. . . . . . . . . . . . 13 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1→(𝒫 𝑊 ∖ {∅}) → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵))
15	13, 14	syl 17	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵))
16		gricushgr.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (Edg‘𝐵)
17		edgval 29084	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐵) = ran (iEdg‘𝐵)
18	16, 17	eqtri 2768	. . . . . . . . . . . . 13 ⊢ 𝐾 = ran (iEdg‘𝐵)
19		f1oeq3 6852	. . . . . . . . . . . . 13 ⊢ (𝐾 = ran (iEdg‘𝐵) → ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 ↔ (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵)))
20	18, 19	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 ↔ (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵))
21	15, 20	sylibr 234	. . . . . . . . . . 11 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾)
22	21	ad3antlr 730	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾)
23		simprl 770	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵))
24	1, 3	ushgrf 29098	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}))
25		f1f1orn 6873	. . . . . . . . . . . . . . 15 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴))
26	24, 25	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴))
27		gricushgr.e	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (Edg‘𝐴)
28		edgval 29084	. . . . . . . . . . . . . . . 16 ⊢ (Edg‘𝐴) = ran (iEdg‘𝐴)
29	27, 28	eqtri 2768	. . . . . . . . . . . . . . 15 ⊢ 𝐸 = ran (iEdg‘𝐴)
30		f1oeq3 6852	. . . . . . . . . . . . . . 15 ⊢ (𝐸 = ran (iEdg‘𝐴) → ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴)))
31	29, 30	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴))
32	26, 31	sylibr 234	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸)
33		f1ocnv 6874	. . . . . . . . . . . . 13 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸 → ^◡(iEdg‘𝐴):𝐸–1-1-onto→dom (iEdg‘𝐴))
34	32, 33	syl 17	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ USHGraph → ^◡(iEdg‘𝐴):𝐸–1-1-onto→dom (iEdg‘𝐴))
35	34	ad3antrrr 729	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ^◡(iEdg‘𝐴):𝐸–1-1-onto→dom (iEdg‘𝐴))
36		f1oco 6885	. . . . . . . . . . 11 ⊢ ((ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ^◡(iEdg‘𝐴):𝐸–1-1-onto→dom (iEdg‘𝐴)) → (ℎ ∘ ^◡(iEdg‘𝐴)):𝐸–1-1-onto→dom (iEdg‘𝐵))
37	23, 35, 36	syl2anc 583	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (ℎ ∘ ^◡(iEdg‘𝐴)):𝐸–1-1-onto→dom (iEdg‘𝐵))
38		f1oco 6885	. . . . . . . . . 10 ⊢ (((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 ∧ (ℎ ∘ ^◡(iEdg‘𝐴)):𝐸–1-1-onto→dom (iEdg‘𝐵)) → ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾)
39	22, 37, 38	syl2anc 583	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾)
40	29	eleq2i 2836	. . . . . . . . . . 11 ⊢ (𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ran (iEdg‘𝐴))
41		f1fn 6818	. . . . . . . . . . . . . . 15 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
42	24, 41	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
43		fvelrnb 6982	. . . . . . . . . . . . . 14 ⊢ ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
44	42, 43	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ USHGraph → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
45	44	ad3antrrr 729	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
46		fveq2 6920	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐴)‘𝑖) = ((iEdg‘𝐴)‘𝑗))
47	46	imaeq2d 6089	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
48		2fveq3 6925	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐵)‘(ℎ‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
49	47, 48	eqeq12d 2756	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
50	49	rspccv 3632	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
51	50	ad2antll 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
52	51	imp 406	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
53		coass 6296	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴)) = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))
54	53	eqcomi 2749	. . . . . . . . . . . . . . . . . . 19 ⊢ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))
55	54	fveq1i 6921	. . . . . . . . . . . . . . . . . 18 ⊢ (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)) = ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗))
56		dff1o4 6870	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴) ↔ ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
57	26, 56	sylib 218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ USHGraph → ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
58	57	simprd 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ USHGraph → ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴))
59	58	ad4antr 731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴))
60		f1of 6862	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
61	26, 60	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
62	61	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
63	62	ffvelcdmda 7118	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴))
64		fvco2 7019	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴) ∧ ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = (((iEdg‘𝐵) ∘ ℎ)‘(^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))))
65	59, 63, 64	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = (((iEdg‘𝐵) ∘ ℎ)‘(^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))))
66	32	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸)
67		f1ocnvfv1 7312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸 ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
68	66, 67	sylan 579	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
69	68	fveq2d 6924	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ℎ)‘(^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))) = (((iEdg‘𝐵) ∘ ℎ)‘𝑗))
70		f1ofn 6863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) → ℎ Fn dom (iEdg‘𝐴))
71	70	ad2antrl 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ℎ Fn dom (iEdg‘𝐴))
72		fvco2 7019	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ Fn dom (iEdg‘𝐴) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ℎ)‘𝑗) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
73	71, 72	sylan 579	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ℎ)‘𝑗) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
74	65, 69, 73	3eqtrd 2784	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
75	55, 74	eqtr2id 2793	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐵)‘(ℎ‘𝑗)) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
76	75	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) ∧ ((iEdg‘𝐴)‘𝑗) = 𝑒) → ((iEdg‘𝐵)‘(ℎ‘𝑗)) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
77		imaeq2 6085	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑗) → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
78	77	eqcoms 2748	. . . . . . . . . . . . . . . . 17 ⊢ (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
79		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
80	78, 79	sylan9eqr 2802	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) ∧ ((iEdg‘𝐴)‘𝑗) = 𝑒) → (𝑓 “ 𝑒) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
81		fveq2 6920	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑗) → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
82	81	eqcoms 2748	. . . . . . . . . . . . . . . . 17 ⊢ (((iEdg‘𝐴)‘𝑗) = 𝑒 → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
83	82	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) ∧ ((iEdg‘𝐴)‘𝑗) = 𝑒) → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
84	76, 80, 83	3eqtr4d 2790	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) ∧ ((iEdg‘𝐴)‘𝑗) = 𝑒) → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))
85	84	ex 412	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) → (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
86	52, 85	mpdan 686	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
87	86	rexlimdva 3161	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
88	45, 87	sylbid 240	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
89	40, 88	biimtrid 242	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ 𝐸 → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
90	89	ralrimiv 3151	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))
91	39, 90	jca 511	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
92		f1oeq1 6850	. . . . . . . . 9 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (𝑔:𝐸–1-1-onto→𝐾 ↔ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾))
93		fveq1 6919	. . . . . . . . . . 11 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (𝑔‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))
94	93	eqeq2d 2751	. . . . . . . . . 10 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
95	94	ralbidv 3184	. . . . . . . . 9 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
96	92, 95	anbi12d 631	. . . . . . . 8 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) ↔ (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))))
97	12, 91, 96	spcedv 3611	. . . . . . 7 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))
98	97	ex 412	. . . . . 6 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
99	98	exlimdv 1932	. . . . 5 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
100	6	cnvex 7965	. . . . . . . . . 10 ⊢ ^◡(iEdg‘𝐵) ∈ V
101		vex 3492	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
102	101, 8	coex 7970	. . . . . . . . . 10 ⊢ (𝑔 ∘ (iEdg‘𝐴)) ∈ V
103	100, 102	coex 7970	. . . . . . . . 9 ⊢ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V
104	103	a1i 11	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V)
105	15	ad3antlr 730	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵))
106		f1ocnv 6874	. . . . . . . . . . 11 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵) → ^◡(iEdg‘𝐵):ran (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐵))
107	105, 106	syl 17	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ^◡(iEdg‘𝐵):ran (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐵))
108		f1oeq23 6853	. . . . . . . . . . . . . 14 ⊢ ((𝐸 = ran (iEdg‘𝐴) ∧ 𝐾 = ran (iEdg‘𝐵)) → (𝑔:𝐸–1-1-onto→𝐾 ↔ 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵)))
109	29, 18, 108	mp2an 691	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐸–1-1-onto→𝐾 ↔ 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
110	109	biimpi 216	. . . . . . . . . . . 12 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
111	110	ad2antrl 727	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
112	26	ad3antrrr 729	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴))
113		f1oco 6885	. . . . . . . . . . 11 ⊢ ((𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵) ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴)) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
114	111, 112, 113	syl2anc 583	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
115		f1oco 6885	. . . . . . . . . 10 ⊢ ((^◡(iEdg‘𝐵):ran (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐵) ∧ (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵)) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵))
116	107, 114, 115	syl2anc 583	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵))
117	61	ad2antrr 725	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
118	117	ffund 6751	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → Fun (iEdg‘𝐴))
119	118	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → Fun (iEdg‘𝐴))
120		fvelrn 7110	. . . . . . . . . . . 12 ⊢ ((Fun (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
121	119, 120	sylan 579	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
122	29	raleqi 3332	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
123	122	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
124	123	ad2antll 728	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
125	124	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
126		imaeq2 6085	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑖)))
127		fveq2 6920	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑔‘𝑒) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
128	126, 127	eqeq12d 2756	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖))))
129	128	rspccva 3634	. . . . . . . . . . . . 13 ⊢ ((∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
130	125, 129	sylan 579	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
131		feq3 6730	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐸 = ran (iEdg‘𝐴) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴)))
132	29, 131	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
133	61, 132	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
134	133	ad2antrr 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
135		f1ofn 6863	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔 Fn 𝐸)
136	135	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔 Fn 𝐸)
137	134, 136	anim12ci 613	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
138	137	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
139		fnfco 6786	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)) Fn dom (iEdg‘𝐴))
140	138, 139	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 ∘ (iEdg‘𝐴)) Fn dom (iEdg‘𝐴))
141		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → 𝑖 ∈ dom (iEdg‘𝐴))
142		fvco2 7019	. . . . . . . . . . . . . 14 ⊢ (((𝑔 ∘ (iEdg‘𝐴)) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
143	140, 141, 142	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
144		f1of 6862	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
145	21, 144	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
146	145	ffund 6751	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ USHGraph → Fun (iEdg‘𝐵))
147		funcocnv2 6887	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun (iEdg‘𝐵) → ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ USHGraph → ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
149	148	eqcomd 2746	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ USHGraph → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)))
150	149	ad5antlr 734	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)))
151	150	coeq1d 5886	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))))
152	151	fveq1d 6922	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = ((((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
153		coass 6296	. . . . . . . . . . . . . . 15 ⊢ (((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = ((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))
154	153	fveq1i 6921	. . . . . . . . . . . . . 14 ⊢ ((((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖)
155	152, 154	eqtrdi 2796	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
156		f1of 6862	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔:𝐸⟶𝐾)
157		eqid 2740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐸 = 𝐸
158	157, 18	feq23i 6741	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:𝐸⟶𝐾 ↔ 𝑔:𝐸⟶ran (iEdg‘𝐵))
159	156, 158	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔:𝐸⟶ran (iEdg‘𝐵))
160	159	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔:𝐸⟶ran (iEdg‘𝐵))
161		f1of 6862	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸 → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
162	32, 161	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
163	162	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
164		fco 6771	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:𝐸⟶ran (iEdg‘𝐵) ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
165	160, 163, 164	syl2anr 596	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
166	165	anim1i 614	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
167	166	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
168		ffvelcdm 7115	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵))
169	167, 168	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵))
170		fvresi 7207	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = ((𝑔 ∘ (iEdg‘𝐴))‘𝑖))
171	169, 170	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = ((𝑔 ∘ (iEdg‘𝐴))‘𝑖))
172	162	ad3antrrr 729	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
173	172	anim1i 614	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
174	173	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
175		fvco3 7021	. . . . . . . . . . . . . . 15 ⊢ (((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
176	174, 175	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
177	171, 176	eqtrd 2780	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
178	143, 155, 177	3eqtr3rd 2789	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔‘((iEdg‘𝐴)‘𝑖)) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
179		dff1o4 6870	. . . . . . . . . . . . . . . . 17 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 ↔ ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ ^◡(iEdg‘𝐵) Fn 𝐾))
180	21, 179	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ USHGraph → ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ ^◡(iEdg‘𝐵) Fn 𝐾))
181	180	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ USHGraph → ^◡(iEdg‘𝐵) Fn 𝐾)
182	181	ad5antlr 734	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ^◡(iEdg‘𝐵) Fn 𝐾)
183	156	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔:𝐸⟶𝐾)
184	134, 183	anim12ci 613	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
185	184	ad2antrr 725	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
186		fco 6771	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾)
187	185, 186	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾)
188		fnfco 6786	. . . . . . . . . . . . . 14 ⊢ ((^◡(iEdg‘𝐵) Fn 𝐾 ∧ (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
189	182, 187, 188	syl2anc 583	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
190		fvco2 7019	. . . . . . . . . . . . 13 ⊢ (((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
191	189, 141, 190	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
192	130, 178, 191	3eqtrd 2784	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
193	121, 192	mpdan 686	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
194	193	ralrimiva 3152	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
195	116, 194	jca 511	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
196		f1oeq1 6850	. . . . . . . . 9 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ↔ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵)))
197		fveq1 6919	. . . . . . . . . . . 12 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (ℎ‘𝑖) = ((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
198	197	fveq2d 6924	. . . . . . . . . . 11 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((iEdg‘𝐵)‘(ℎ‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
199	198	eqeq2d 2751	. . . . . . . . . 10 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
200	199	ralbidv 3184	. . . . . . . . 9 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
201	196, 200	anbi12d 631	. . . . . . . 8 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) ↔ ((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))))
202	104, 195, 201	spcedv 3611	. . . . . . 7 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))))
203	202	ex 412	. . . . . 6 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))))
204	203	exlimdv 1932	. . . . 5 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))))
205	99, 204	impbid 212	. . . 4 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) ↔ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
206	205	pm5.32da 578	. . 3 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → ((𝑓:𝑉–1-1-onto→𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ↔ (𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
207	206	exbidv 1920	. 2 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
208	5, 207	bitrd 279	1 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 ≃_𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1537 ∃wex 1777 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 Vcvv 3488 ∖ cdif 3973 ∅c0 4352 𝒫 cpw 4622 {csn 4648 class class class wbr 5166 I cid 5592 ^◡ccnv 5699 dom cdm 5700 ran crn 5701 ↾ cres 5702 “ cima 5703 ∘ ccom 5704 Fun wfun 6567 Fn wfn 6568 ⟶wf 6569 –1-1→wf1 6570 –1-1-onto→wf1o 6572 ‘cfv 6573 Vtxcvtx 29031 iEdgciedg 29032 Edgcedg 29082 USHGraphcushgr 29092 ≃_𝑔𝑟 cgric 47746

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-ov 7451 df-oprab 7452 df-mpo 7453 df-1st 8030 df-2nd 8031 df-1o 8522 df-map 8886 df-edg 29083 df-ushgr 29094 df-grim 47748 df-gric 47751

This theorem is referenced by: (None)

W3C validator