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 43990

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 2821	. . 3 ⊢ (iEdg‘𝐴) = (iEdg‘𝐴)
4		eqid 2821	. . 3 ⊢ (iEdg‘𝐵) = (iEdg‘𝐵)
5	1, 2, 3, 4	isomgr 43987	. 2 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))))))
6		fvex 6682	. . . . . . . . . 10 ⊢ (iEdg‘𝐵) ∈ V
7		vex 3497	. . . . . . . . . . 11 ⊢ ℎ ∈ V
8		fvex 6682	. . . . . . . . . . . 12 ⊢ (iEdg‘𝐴) ∈ V
9	8	cnvex 7629	. . . . . . . . . . 11 ⊢ ^◡(iEdg‘𝐴) ∈ V
10	7, 9	coex 7634	. . . . . . . . . 10 ⊢ (ℎ ∘ ^◡(iEdg‘𝐴)) ∈ V
11	6, 10	coex 7634	. . . . . . . . 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 26847	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1→(𝒫 𝑊 ∖ {∅}))
14		f1f1orn 6625	. . . . . . . . . . . . 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 26833	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐵) = ran (iEdg‘𝐵)
18	16, 17	eqtri 2844	. . . . . . . . . . . . 13 ⊢ 𝐾 = ran (iEdg‘𝐵)
19		f1oeq3 6605	. . . . . . . . . . . . 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 236	. . . . . . . . . . 11 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾)
22	21	ad3antlr 729	. . . . . . . . . 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 769	. . . . . . . . . . 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 26847	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}))
25		f1f1orn 6625	. . . . . . . . . . . . . . 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 26833	. . . . . . . . . . . . . . . 16 ⊢ (Edg‘𝐴) = ran (iEdg‘𝐴)
29	27, 28	eqtri 2844	. . . . . . . . . . . . . . 15 ⊢ 𝐸 = ran (iEdg‘𝐴)
30		f1oeq3 6605	. . . . . . . . . . . . . . 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 236	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸)
33		f1ocnv 6626	. . . . . . . . . . . . 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 728	. . . . . . . . . . 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 6636	. . . . . . . . . . 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 586	. . . . . . . . . 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 6636	. . . . . . . . . 10 ⊢ (((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 ∧ (ℎ ∘ ^◡(iEdg‘𝐴)):𝐸–1-1-onto→dom (iEdg‘𝐵)) → ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾)
39	22, 37, 38	syl2anc 586	. . . . . . . . 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 2904	. . . . . . . . . . 11 ⊢ (𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ran (iEdg‘𝐴))
41		f1fn 6575	. . . . . . . . . . . . . . 15 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
42	24, 41	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
43		fvelrnb 6725	. . . . . . . . . . . . . 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 728	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
46		fveq2 6669	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐴)‘𝑖) = ((iEdg‘𝐴)‘𝑗))
47	46	imaeq2d 5928	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
48		2fveq3 6674	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐵)‘(ℎ‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
49	47, 48	eqeq12d 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
50	49	rspccv 3619	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
51	50	ad2antll 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
52	51	imp 409	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
53		coass 6117	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴)) = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))
54	53	eqcomi 2830	. . . . . . . . . . . . . . . . . . 19 ⊢ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))
55	54	fveq1i 6670	. . . . . . . . . . . . . . . . . 18 ⊢ (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)) = ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗))
56		dff1o4 6622	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴) ↔ ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
57	26, 56	sylib 220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ USHGraph → ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
58	57	simprd 498	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ USHGraph → ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴))
59	58	ad4antr 730	. . . . . . . . . . . . . . . . . . . 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 6614	. . . . . . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
63	62	ffvelrnda 6850	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴))
64		fvco2 6757	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴) ∧ ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = (((iEdg‘𝐵) ∘ ℎ)‘(^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))))
65	59, 63, 64	syl2anc 586	. . . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . . . . . . . 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 7032	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸 ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
68	66, 67	sylan 582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
69	68	fveq2d 6673	. . . . . . . . . . . . . . . . . . 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 6615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) → ℎ Fn dom (iEdg‘𝐴))
71	70	ad2antrl 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ℎ Fn dom (iEdg‘𝐴))
72		fvco2 6757	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ Fn dom (iEdg‘𝐴) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ℎ)‘𝑗) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
73	71, 72	sylan 582	. . . . . . . . . . . . . . . . . . 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 2860	. . . . . . . . . . . . . . . . . 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	syl5req 2869	. . . . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . . 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 5924	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑗) → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
78	77	eqcoms 2829	. . . . . . . . . . . . . . . . 17 ⊢ (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
79		simpr 487	. . . . . . . . . . . . . . . . 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 2878	. . . . . . . . . . . . . . . 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 6669	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑗) → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
82	81	eqcoms 2829	. . . . . . . . . . . . . . . . 17 ⊢ (((iEdg‘𝐴)‘𝑗) = 𝑒 → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
83	82	adantl 484	. . . . . . . . . . . . . . . 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 2866	. . . . . . . . . . . . . . 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 415	. . . . . . . . . . . . . 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 685	. . . . . . . . . . . . 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 3284	. . . . . . . . . . . 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 242	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
89	40, 88	syl5bi 244	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ 𝐸 → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
90	89	ralrimiv 3181	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))
91	39, 90	jca 514	. . . . . . . 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 6603	. . . . . . . . 9 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (𝑔:𝐸–1-1-onto→𝐾 ↔ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸–1-1-onto→𝐾))
93		fveq1 6668	. . . . . . . . . . 11 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (𝑔‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))
94	93	eqeq2d 2832	. . . . . . . . . 10 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
95	94	ralbidv 3197	. . . . . . . . 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 3598	. . . . . . 7 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))
98	97	ex 415	. . . . . 6 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
99	98	exlimdv 1930	. . . . 5 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
100	6	cnvex 7629	. . . . . . . . . 10 ⊢ ^◡(iEdg‘𝐵) ∈ V
101		vex 3497	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
102	101, 8	coex 7634	. . . . . . . . . 10 ⊢ (𝑔 ∘ (iEdg‘𝐴)) ∈ V
103	100, 102	coex 7634	. . . . . . . . 9 ⊢ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V
104	103	a1i 11	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V)
105	15	ad3antlr 729	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵))
106		f1ocnv 6626	. . . . . . . . . . 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 6606	. . . . . . . . . . . . . 14 ⊢ ((𝐸 = ran (iEdg‘𝐴) ∧ 𝐾 = ran (iEdg‘𝐵)) → (𝑔:𝐸–1-1-onto→𝐾 ↔ 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵)))
109	29, 18, 108	mp2an 690	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐸–1-1-onto→𝐾 ↔ 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
110	109	biimpi 218	. . . . . . . . . . . 12 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
111	110	ad2antrl 726	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
112	26	ad3antrrr 728	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴))
113		f1oco 6636	. . . . . . . . . . 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 586	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
115		f1oco 6636	. . . . . . . . . 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 586	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵))
117	61	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
118	117	ffund 6517	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → Fun (iEdg‘𝐴))
119	118	adantr 483	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → Fun (iEdg‘𝐴))
120		fvelrn 6843	. . . . . . . . . . . 12 ⊢ ((Fun (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
121	119, 120	sylan 582	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
122	29	raleqi 3413	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
123	122	biimpi 218	. . . . . . . . . . . . . . 15 ⊢ (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
124	123	ad2antll 727	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
125	124	adantr 483	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
126		imaeq2 5924	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑖)))
127		fveq2 6669	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑔‘𝑒) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
128	126, 127	eqeq12d 2837	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖))))
129	128	rspccva 3621	. . . . . . . . . . . . 13 ⊢ ((∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
130	125, 129	sylan 582	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
131		feq3 6496	. . . . . . . . . . . . . . . . . . . 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 236	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
134	133	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
135		f1ofn 6615	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔 Fn 𝐸)
136	135	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔 Fn 𝐸)
137	134, 136	anim12ci 615	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
138	137	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
139		fnfco 6542	. . . . . . . . . . . . . . 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		simpr 487	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → 𝑖 ∈ dom (iEdg‘𝐴))
142	141	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → 𝑖 ∈ dom (iEdg‘𝐴))
143		fvco2 6757	. . . . . . . . . . . . . 14 ⊢ (((𝑔 ∘ (iEdg‘𝐴)) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
144	140, 142, 143	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
145		f1of 6614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
146	21, 145	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
147	146	ffund 6517	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ USHGraph → Fun (iEdg‘𝐵))
148		funcocnv2 6638	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun (iEdg‘𝐵) → ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
149	147, 148	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ USHGraph → ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
150	149	eqcomd 2827	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ USHGraph → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)))
151	150	ad5antlr 733	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)))
152	151	coeq1d 5731	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))))
153	152	fveq1d 6671	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = ((((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
154		coass 6117	. . . . . . . . . . . . . . 15 ⊢ (((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = ((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))
155	154	fveq1i 6670	. . . . . . . . . . . . . 14 ⊢ ((((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖)
156	153, 155	syl6eq 2872	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
157		f1of 6614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔:𝐸⟶𝐾)
158		eqid 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐸 = 𝐸
159	158, 18	feq23i 6507	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:𝐸⟶𝐾 ↔ 𝑔:𝐸⟶ran (iEdg‘𝐵))
160	157, 159	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:𝐸–1-1-onto→𝐾 → 𝑔:𝐸⟶ran (iEdg‘𝐵))
161	160	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔:𝐸⟶ran (iEdg‘𝐵))
162		f1of 6614	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→𝐸 → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
163	32, 162	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
164	163	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
165		fco 6530	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:𝐸⟶ran (iEdg‘𝐵) ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
166	161, 164, 165	syl2anr 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
167	166	anim1i 616	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
168	167	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
169		ffvelrn 6848	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵))
170	168, 169	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵))
171		fvresi 6934	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = ((𝑔 ∘ (iEdg‘𝐴))‘𝑖))
172	170, 171	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = ((𝑔 ∘ (iEdg‘𝐴))‘𝑖))
173	163	ad3antrrr 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
174	173	anim1i 616	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
175	174	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
176		fvco3 6759	. . . . . . . . . . . . . . 15 ⊢ (((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
177	175, 176	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
178	172, 177	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
179	144, 156, 178	3eqtr3rd 2865	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔‘((iEdg‘𝐴)‘𝑖)) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
180		dff1o4 6622	. . . . . . . . . . . . . . . . 17 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→𝐾 ↔ ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ ^◡(iEdg‘𝐵) Fn 𝐾))
181	21, 180	sylib 220	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ USHGraph → ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ ^◡(iEdg‘𝐵) Fn 𝐾))
182	181	simprd 498	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ USHGraph → ^◡(iEdg‘𝐵) Fn 𝐾)
183	182	ad5antlr 733	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ^◡(iEdg‘𝐵) Fn 𝐾)
184	157	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔:𝐸⟶𝐾)
185	134, 184	anim12ci 615	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
186	185	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
187		fco 6530	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾)
188	186, 187	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾)
189		fnfco 6542	. . . . . . . . . . . . . 14 ⊢ ((^◡(iEdg‘𝐵) Fn 𝐾 ∧ (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
190	183, 188, 189	syl2anc 586	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
191		fvco2 6757	. . . . . . . . . . . . 13 ⊢ (((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
192	190, 142, 191	syl2anc 586	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
193	130, 179, 192	3eqtrd 2860	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
194	121, 193	mpdan 685	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
195	194	ralrimiva 3182	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
196	116, 195	jca 514	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
197		f1oeq1 6603	. . . . . . . . 9 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ↔ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵)))
198		fveq1 6668	. . . . . . . . . . . 12 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (ℎ‘𝑖) = ((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
199	198	fveq2d 6673	. . . . . . . . . . 11 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((iEdg‘𝐵)‘(ℎ‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
200	199	eqeq2d 2832	. . . . . . . . . 10 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
201	200	ralbidv 3197	. . . . . . . . 9 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
202	197, 201	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‘𝐴)))‘𝑖)))))
203	104, 196, 202	spcedv 3598	. . . . . . 7 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) ∧ (𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))))
204	203	ex 415	. . . . . 6 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → ((𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))))
205	204	exlimdv 1930	. . . . 5 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))))
206	99, 205	impbid 214	. . . 4 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉–1-1-onto→𝑊) → (∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) ↔ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
207	206	pm5.32da 581	. . 3 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → ((𝑓:𝑉–1-1-onto→𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ↔ (𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
208	207	exbidv 1918	. 2 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
209	5, 208	bitrd 281	1 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:𝑉–1-1-onto→𝑊 ∧ ∃𝑔(𝑔:𝐸–1-1-onto→𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1533 ∃wex 1776 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 Vcvv 3494 ∖ cdif 3932 ∅c0 4290 𝒫 cpw 4538 {csn 4566 class class class wbr 5065 I cid 5458 ^◡ccnv 5553 dom cdm 5554 ran crn 5555 ↾ cres 5556 “ cima 5557 ∘ ccom 5558 Fun wfun 6348 Fn wfn 6349 ⟶wf 6350 –1-1→wf1 6351 –1-1-onto→wf1o 6353 ‘cfv 6354 Vtxcvtx 26780 iEdgciedg 26781 Edgcedg 26831 USHGraphcushgr 26841 IsomGr cisomgr 43983

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5202 ax-nul 5209 ax-pow 5265 ax-pr 5329 ax-un 7460

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4567 df-pr 4569 df-op 4573 df-uni 4838 df-br 5066 df-opab 5128 df-mpt 5146 df-id 5459 df-xp 5560 df-rel 5561 df-cnv 5562 df-co 5563 df-dm 5564 df-rn 5565 df-res 5566 df-ima 5567 df-iota 6313 df-fun 6356 df-fn 6357 df-f 6358 df-f1 6359 df-fo 6360 df-f1o 6361 df-fv 6362 df-edg 26832 df-ushgr 26843 df-isomgr 43985

This theorem is referenced by: isomuspgr 43998

W3C validator