isomushgr - Mathbox for Alexander van der Vekens

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

Theorem isomushgr 46793

Description: The isomorphy relation for two simple hypergraphs. (Contributed by AV, 28-Nov-2022.)

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

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

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

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

Step	Hyp	Ref	Expression
1		isomushgr.v	. . 3 ⊢ 𝑉 = (Vtx‘𝐴)
2		isomushgr.w	. . 3 ⊢ 𝑊 = (Vtx‘𝐵)
3		eqid 2731	. . 3 ⊢ (iEdg‘𝐴) = (iEdg‘𝐴)
4		eqid 2731	. . 3 ⊢ (iEdg‘𝐵) = (iEdg‘𝐵)
5	1, 2, 3, 4	isomgr 46790	. 2 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))))))
6		fvex 6904	. . . . . . . . . 10 ⊢ (iEdg‘𝐵) ∈ V
7		vex 3477	. . . . . . . . . . 11 ⊢ ℎ ∈ V
8		fvex 6904	. . . . . . . . . . . 12 ⊢ (iEdg‘𝐴) ∈ V
9	8	cnvex 7920	. . . . . . . . . . 11 ⊢ ^◡(iEdg‘𝐴) ∈ V
10	7, 9	coex 7925	. . . . . . . . . 10 ⊢ (ℎ ∘ ^◡(iEdg‘𝐴)) ∈ V
11	6, 10	coex 7925	. . . . . . . . 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 28591	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1→(𝒫 𝑊 ∖ {∅}))
14		f1f1orn 6844	. . . . . . . . . . . . 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		isomushgr.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (Edg‘𝐵)
17		edgval 28577	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐵) = ran (iEdg‘𝐵)
18	16, 17	eqtri 2759	. . . . . . . . . . . . 13 ⊢ 𝐾 = ran (iEdg‘𝐵)
19		f1oeq3 6823	. . . . . . . . . . . . 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 233	. . . . . . . . . . 11 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾)
22	21	ad3antlr 728	. . . . . . . . . 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 768	. . . . . . . . . . 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 28591	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}))
25		f1f1orn 6844	. . . . . . . . . . . . . . 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		isomushgr.e	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (Edg‘𝐴)
28		edgval 28577	. . . . . . . . . . . . . . . 16 ⊢ (Edg‘𝐴) = ran (iEdg‘𝐴)
29	27, 28	eqtri 2759	. . . . . . . . . . . . . . 15 ⊢ 𝐸 = ran (iEdg‘𝐴)
30		f1oeq3 6823	. . . . . . . . . . . . . . 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 233	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸)
33		f1ocnv 6845	. . . . . . . . . . . . 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 727	. . . . . . . . . . 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 6856	. . . . . . . . . . 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 6856	. . . . . . . . . 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 2824	. . . . . . . . . . 11 ⊢ (𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ran (iEdg‘𝐴))
41		f1fn 6788	. . . . . . . . . . . . . . 15 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
42	24, 41	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
43		fvelrnb 6952	. . . . . . . . . . . . . 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 727	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
46		fveq2 6891	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐴)‘𝑖) = ((iEdg‘𝐴)‘𝑗))
47	46	imaeq2d 6059	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
48		2fveq3 6896	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐵)‘(ℎ‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
49	47, 48	eqeq12d 2747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
50	49	rspccv 3609	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
51	50	ad2antll 726	. . . . . . . . . . . . . . 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 6264	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴)) = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))
54	53	eqcomi 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))
55	54	fveq1i 6892	. . . . . . . . . . . . . . . . . 18 ⊢ (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)) = ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗))
56		dff1o4 6841	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴) ↔ ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
57	26, 56	sylib 217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ USHGraph → ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
58	57	simprd 495	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ USHGraph → ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴))
59	58	ad4antr 729	. . . . . . . . . . . . . . . . . . . 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 6833	. . . . . . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . . . 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 7086	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴))
64		fvco2 6988	. . . . . . . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . . . . . 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 7277	. . . . . . . . . . . . . . . . . . . . 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 6895	. . . . . . . . . . . . . . . . . . 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 6834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) → ℎ Fn dom (iEdg‘𝐴))
71	70	ad2antrl 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ℎ Fn dom (iEdg‘𝐴))
72		fvco2 6988	. . . . . . . . . . . . . . . . . . . 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 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 723	. . . . . . . . . . . . . . . 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 6055	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑗) → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
78	77	eqcoms 2739	. . . . . . . . . . . . . . . . 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 6891	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑗) → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
82	81	eqcoms 2739	. . . . . . . . . . . . . . . . 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 684	. . . . . . . . . . . . 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 3154	. . . . . . . . . . . 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 239	. . . . . . . . . . 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 241	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ 𝐸 → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
90	89	ralrimiv 3144	. . . . . . . . 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 6821	. . . . . . . . 9 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (𝑔:𝐸–1-1-onto→𝐾 ↔ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾))
93		fveq1 6890	. . . . . . . . . . 11 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (𝑔‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))
94	93	eqeq2d 2742	. . . . . . . . . 10 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
95	94	ralbidv 3176	. . . . . . . . 9 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
96	92, 95	anbi12d 630	. . . . . . . 8 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) ↔ (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))))
97	12, 91, 96	spcedv 3588	. . . . . . 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 1935	. . . . 5 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
100	6	cnvex 7920	. . . . . . . . . 10 ⊢ ^◡(iEdg‘𝐵) ∈ V
101		vex 3477	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
102	101, 8	coex 7925	. . . . . . . . . 10 ⊢ (𝑔 ∘ (iEdg‘𝐴)) ∈ V
103	100, 102	coex 7925	. . . . . . . . 9 ⊢ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V
104	103	a1i 11	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V)
105	15	ad3antlr 728	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵))
106		f1ocnv 6845	. . . . . . . . . . 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 6824	. . . . . . . . . . . . . 14 ⊢ ((𝐸 = ran (iEdg‘𝐴) ∧ 𝐾 = ran (iEdg‘𝐵)) → (𝑔:𝐸–1-1-onto→𝐾 ↔ 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵)))
109	29, 18, 108	mp2an 689	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐸–1-1-onto→𝐾 ↔ 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
110	109	biimpi 215	. . . . . . . . . . . 12 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
111	110	ad2antrl 725	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
112	26	ad3antrrr 727	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴))
113		f1oco 6856	. . . . . . . . . . 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 6856	. . . . . . . . . 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 723	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
118	117	ffund 6721	. . . . . . . . . . . . 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 7078	. . . . . . . . . . . 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 3322	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
123	122	biimpi 215	. . . . . . . . . . . . . . 15 ⊢ (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
124	123	ad2antll 726	. . . . . . . . . . . . . 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 6055	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑖)))
127		fveq2 6891	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑔‘𝑒) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
128	126, 127	eqeq12d 2747	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖))))
129	128	rspccva 3611	. . . . . . . . . . . . 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 6700	. . . . . . . . . . . . . . . . . . . 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 233	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
134	133	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
135		f1ofn 6834	. . . . . . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
139		fnfco 6756	. . . . . . . . . . . . . . 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 766	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → 𝑖 ∈ dom (iEdg‘𝐴))
142		fvco2 6988	. . . . . . . . . . . . . 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 6833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
145	21, 144	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
146	145	ffund 6721	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ USHGraph → Fun (iEdg‘𝐵))
147		funcocnv2 6858	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun (iEdg‘𝐵) → ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
148	146, 147	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ USHGraph → ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
149	148	eqcomd 2737	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ USHGraph → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)))
150	149	ad5antlr 732	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)))
151	150	coeq1d 5861	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))))
152	151	fveq1d 6893	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = ((((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
153		coass 6264	. . . . . . . . . . . . . . 15 ⊢ (((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = ((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))
154	153	fveq1i 6892	. . . . . . . . . . . . . 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 6833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔:𝐸⟶𝐾)
157		eqid 2731	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐸 = 𝐸
158	157, 18	feq23i 6711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:𝐸⟶𝐾 ↔ 𝑔:𝐸⟶ran (iEdg‘𝐵))
159	156, 158	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔:𝐸⟶ran (iEdg‘𝐵))
160	159	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔:𝐸⟶ran (iEdg‘𝐵))
161		f1of 6833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸 → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
162	32, 161	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
163	162	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
164		fco 6741	. . . . . . . . . . . . . . . . . . 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 7083	. . . . . . . . . . . . . . . 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 7173	. . . . . . . . . . . . . . 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 727	. . . . . . . . . . . . . . . . 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 6990	. . . . . . . . . . . . . . 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 6841	. . . . . . . . . . . . . . . . 17 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 ↔ ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ ^◡(iEdg‘𝐵) Fn 𝐾))
180	21, 179	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ USHGraph → ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ ^◡(iEdg‘𝐵) Fn 𝐾))
181	180	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ USHGraph → ^◡(iEdg‘𝐵) Fn 𝐾)
182	181	ad5antlr 732	. . . . . . . . . . . . . 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 723	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
186		fco 6741	. . . . . . . . . . . . . . 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 6756	. . . . . . . . . . . . . 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 6988	. . . . . . . . . . . . 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 2775	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
193	121, 192	mpdan 684	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
194	193	ralrimiva 3145	. . . . . . . . 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 6821	. . . . . . . . 9 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ↔ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵)))
197		fveq1 6890	. . . . . . . . . . . 12 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (ℎ‘𝑖) = ((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
198	197	fveq2d 6895	. . . . . . . . . . 11 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((iEdg‘𝐵)‘(ℎ‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
199	198	eqeq2d 2742	. . . . . . . . . 10 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
200	199	ralbidv 3176	. . . . . . . . 9 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
201	196, 200	anbi12d 630	. . . . . . . 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 3588	. . . . . . 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 1935	. . . . 5 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))))
205	99, 204	impbid 211	. . . 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 1923	. 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) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 = wceq 1540 ∃wex 1780 ∈ wcel 2105 ∀wral 3060 ∃wrex 3069 Vcvv 3473 ∖ cdif 3945 ∅c0 4322 𝒫 cpw 4602 {csn 4628 class class class wbr 5148 I cid 5573 ^◡ccnv 5675 dom cdm 5676 ran crn 5677 ↾ cres 5678 “ cima 5679 ∘ ccom 5680 Fun wfun 6537 Fn wfn 6538 ⟶wf 6539 –1-1→wf1 6540 –1-1-onto→wf1o 6542 ‘cfv 6543 Vtxcvtx 28524 iEdgciedg 28525 Edgcedg 28575 USHGraphcushgr 28585 IsomGr cisomgr 46786

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-sbc 3778 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-edg 28576 df-ushgr 28587 df-isomgr 46788

This theorem is referenced by: isomuspgr 46801

W3C validator