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 47897

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 2736	. . 3 ⊢ (iEdg‘𝐴) = (iEdg‘𝐴)
4		eqid 2736	. . 3 ⊢ (iEdg‘𝐵) = (iEdg‘𝐵)
5	1, 2, 3, 4	dfgric2 47895	. 2 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 ≃_𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))))))
6		fvex 6894	. . . . . . . . . 10 ⊢ (iEdg‘𝐵) ∈ V
7		vex 3468	. . . . . . . . . . 11 ⊢ ℎ ∈ V
8		fvex 6894	. . . . . . . . . . . 12 ⊢ (iEdg‘𝐴) ∈ V
9	8	cnvex 7926	. . . . . . . . . . 11 ⊢ ^◡(iEdg‘𝐴) ∈ V
10	7, 9	coex 7931	. . . . . . . . . 10 ⊢ (ℎ ∘ ^◡(iEdg‘𝐴)) ∈ V
11	6, 10	coex 7931	. . . . . . . . 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 29047	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1→(𝒫 𝑊 ∖ {∅}))
14		f1f1orn 6834	. . . . . . . . . . . . 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 29033	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐵) = ran (iEdg‘𝐵)
18	16, 17	eqtri 2759	. . . . . . . . . . . . 13 ⊢ 𝐾 = ran (iEdg‘𝐵)
19		f1oeq3 6813	. . . . . . . . . . . . 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 731	. . . . . . . . . 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 29047	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}))
25		f1f1orn 6834	. . . . . . . . . . . . . . 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 29033	. . . . . . . . . . . . . . . 16 ⊢ (Edg‘𝐴) = ran (iEdg‘𝐴)
29	27, 28	eqtri 2759	. . . . . . . . . . . . . . 15 ⊢ 𝐸 = ran (iEdg‘𝐴)
30		f1oeq3 6813	. . . . . . . . . . . . . . 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 6835	. . . . . . . . . . . . 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 730	. . . . . . . . . . 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 6846	. . . . . . . . . . 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 584	. . . . . . . . . 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 6846	. . . . . . . . . 10 ⊢ (((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 ∧ (ℎ ∘ ^◡(iEdg‘𝐴)):𝐸–1-1-onto→dom (iEdg‘𝐵)) → ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾)
39	22, 37, 38	syl2anc 584	. . . . . . . . 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 2827	. . . . . . . . . . 11 ⊢ (𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ran (iEdg‘𝐴))
41		f1fn 6780	. . . . . . . . . . . . . . 15 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
42	24, 41	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
43		fvelrnb 6944	. . . . . . . . . . . . . 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 730	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
46		fveq2 6881	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐴)‘𝑖) = ((iEdg‘𝐴)‘𝑗))
47	46	imaeq2d 6052	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
48		2fveq3 6886	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐵)‘(ℎ‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
49	47, 48	eqeq12d 2752	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
50	49	rspccv 3603	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
51	50	ad2antll 729	. . . . . . . . . . . . . . 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 6259	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴)) = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))
54	53	eqcomi 2745	. . . . . . . . . . . . . . . . . . 19 ⊢ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))
55	54	fveq1i 6882	. . . . . . . . . . . . . . . . . 18 ⊢ (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)) = ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗))
56		dff1o4 6831	. . . . . . . . . . . . . . . . . . . . . . 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 732	. . . . . . . . . . . . . . . . . . . 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 6823	. . . . . . . . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . . . 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 7079	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴))
64		fvco2 6981	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴) ∧ ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = (((iEdg‘𝐵) ∘ ℎ)‘(^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))))
65	59, 63, 64	syl2anc 584	. . . . . . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . . . . . 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 7274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸 ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
68	66, 67	sylan 580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
69	68	fveq2d 6885	. . . . . . . . . . . . . . . . . . 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 6824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) → ℎ Fn dom (iEdg‘𝐴))
71	70	ad2antrl 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ℎ Fn dom (iEdg‘𝐴))
72		fvco2 6981	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ Fn dom (iEdg‘𝐴) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ℎ)‘𝑗) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
73	71, 72	sylan 580	. . . . . . . . . . . . . . . . . . 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 2775	. . . . . . . . . . . . . . . . . 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 2784	. . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . 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 6048	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑗) → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
78	77	eqcoms 2744	. . . . . . . . . . . . . . . . 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 2793	. . . . . . . . . . . . . . . 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 6881	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑗) → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
82	81	eqcoms 2744	. . . . . . . . . . . . . . . . 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 2781	. . . . . . . . . . . . . . 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 687	. . . . . . . . . . . . 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 3142	. . . . . . . . . . . 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 3132	. . . . . . . . 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 6811	. . . . . . . . 9 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (𝑔:𝐸–1-1-onto→𝐾 ↔ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾))
93		fveq1 6880	. . . . . . . . . . 11 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (𝑔‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))
94	93	eqeq2d 2747	. . . . . . . . . 10 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
95	94	ralbidv 3164	. . . . . . . . 9 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
96	92, 95	anbi12d 632	. . . . . . . 8 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) ↔ (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))))
97	12, 91, 96	spcedv 3582	. . . . . . 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 1933	. . . . 5 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
100	6	cnvex 7926	. . . . . . . . . 10 ⊢ ^◡(iEdg‘𝐵) ∈ V
101		vex 3468	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
102	101, 8	coex 7931	. . . . . . . . . 10 ⊢ (𝑔 ∘ (iEdg‘𝐴)) ∈ V
103	100, 102	coex 7931	. . . . . . . . 9 ⊢ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V
104	103	a1i 11	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V)
105	15	ad3antlr 731	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵))
106		f1ocnv 6835	. . . . . . . . . . 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 6814	. . . . . . . . . . . . . 14 ⊢ ((𝐸 = ran (iEdg‘𝐴) ∧ 𝐾 = ran (iEdg‘𝐵)) → (𝑔:𝐸–1-1-onto→𝐾 ↔ 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵)))
109	29, 18, 108	mp2an 692	. . . . . . . . . . . . 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 728	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
112	26	ad3antrrr 730	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴))
113		f1oco 6846	. . . . . . . . . . 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 584	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
115		f1oco 6846	. . . . . . . . . 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 584	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵))
117	61	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
118	117	ffund 6715	. . . . . . . . . . . . 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 7071	. . . . . . . . . . . 12 ⊢ ((Fun (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
121	119, 120	sylan 580	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
122	29	raleqi 3307	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
123	122	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
124	123	ad2antll 729	. . . . . . . . . . . . . 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 6048	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑖)))
127		fveq2 6881	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑔‘𝑒) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
128	126, 127	eqeq12d 2752	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖))))
129	128	rspccva 3605	. . . . . . . . . . . . 13 ⊢ ((∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
130	125, 129	sylan 580	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
131		feq3 6693	. . . . . . . . . . . . . . . . . . . 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 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
135		f1ofn 6824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔 Fn 𝐸)
136	135	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔 Fn 𝐸)
137	134, 136	anim12ci 614	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
138	137	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
139		fnfco 6748	. . . . . . . . . . . . . . 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 6981	. . . . . . . . . . . . . 14 ⊢ (((𝑔 ∘ (iEdg‘𝐴)) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
143	140, 141, 142	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
144		f1of 6823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
145	21, 144	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
146	145	ffund 6715	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ USHGraph → Fun (iEdg‘𝐵))
147		funcocnv2 6848	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun (iEdg‘𝐵) → ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ USHGraph → ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
149	148	eqcomd 2742	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ USHGraph → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)))
150	149	ad5antlr 735	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)))
151	150	coeq1d 5846	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))))
152	151	fveq1d 6883	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = ((((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
153		coass 6259	. . . . . . . . . . . . . . 15 ⊢ (((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = ((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))
154	153	fveq1i 6882	. . . . . . . . . . . . . 14 ⊢ ((((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖)
155	152, 154	eqtrdi 2787	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
156		f1of 6823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔:𝐸⟶𝐾)
157		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐸 = 𝐸
158	157, 18	feq23i 6705	. . . . . . . . . . . . . . . . . . . . 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 6823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸 → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
162	32, 161	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
163	162	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
164		fco 6735	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:𝐸⟶ran (iEdg‘𝐵) ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
165	160, 163, 164	syl2anr 597	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
166	165	anim1i 615	. . . . . . . . . . . . . . . . 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 7076	. . . . . . . . . . . . . . . 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 7170	. . . . . . . . . . . . . . 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 730	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
173	172	anim1i 615	. . . . . . . . . . . . . . . 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 6983	. . . . . . . . . . . . . . 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 2771	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
178	143, 155, 177	3eqtr3rd 2780	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔‘((iEdg‘𝐴)‘𝑖)) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
179		dff1o4 6831	. . . . . . . . . . . . . . . . 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 735	. . . . . . . . . . . . . 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 614	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
185	184	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
186		fco 6735	. . . . . . . . . . . . . . 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 6748	. . . . . . . . . . . . . 14 ⊢ ((^◡(iEdg‘𝐵) Fn 𝐾 ∧ (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
189	182, 187, 188	syl2anc 584	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
190		fvco2 6981	. . . . . . . . . . . . 13 ⊢ (((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
191	189, 141, 190	syl2anc 584	. . . . . . . . . . . 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 2775	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
193	121, 192	mpdan 687	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
194	193	ralrimiva 3133	. . . . . . . . 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 6811	. . . . . . . . 9 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ↔ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵)))
197		fveq1 6880	. . . . . . . . . . . 12 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (ℎ‘𝑖) = ((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
198	197	fveq2d 6885	. . . . . . . . . . 11 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((iEdg‘𝐵)‘(ℎ‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
199	198	eqeq2d 2747	. . . . . . . . . 10 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
200	199	ralbidv 3164	. . . . . . . . 9 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
201	196, 200	anbi12d 632	. . . . . . . 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 3582	. . . . . . 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 1933	. . . . 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 579	. . 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 1921	. 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 1540 ∃wex 1779 ∈ wcel 2109 ∀wral 3052 ∃wrex 3061 Vcvv 3464 ∖ cdif 3928 ∅c0 4313 𝒫 cpw 4580 {csn 4606 class class class wbr 5124 I cid 5552 ^◡ccnv 5658 dom cdm 5659 ran crn 5660 ↾ cres 5661 “ cima 5662 ∘ ccom 5663 Fun wfun 6530 Fn wfn 6531 ⟶wf 6532 –1-1→wf1 6533 –1-1-onto→wf1o 6535 ‘cfv 6536 Vtxcvtx 28980 iEdgciedg 28981 Edgcedg 29031 USHGraphcushgr 29041 ≃_𝑔𝑟 cgric 47856

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-id 5553 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-1st 7993 df-2nd 7994 df-1o 8485 df-map 8847 df-edg 29032 df-ushgr 29043 df-grim 47858 df-gric 47861

This theorem is referenced by: isubgr3stgr 47954

W3C validator