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 49282

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-1onto𝑊 ∧ ∃𝑔(𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))

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 2763	. . 3 ⊢ (iEdg‘𝐴) = (iEdg‘𝐴)
4		eqid 2763	. . 3 ⊢ (iEdg‘𝐵) = (iEdg‘𝐵)
5	1, 2, 3, 4	dfgric2 49280	. 2 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 ≃_𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉⟶1-1onto𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))))))
6		fvex 6927	. . . . . . . . . 10 ⊢ (iEdg‘𝐵) ∈ V
7		vex 3458	. . . . . . . . . . 11 ⊢ ℎ ∈ V
8		fvex 6927	. . . . . . . . . . . 12 ⊢ (iEdg‘𝐴) ∈ V
9	8	cnvex 7969	. . . . . . . . . . 11 ⊢ ^◡(iEdg‘𝐴) ∈ V
10	7, 9	coex 7974	. . . . . . . . . 10 ⊢ (ℎ ∘ ^◡(iEdg‘𝐴)) ∈ V
11	6, 10	coex 7974	. . . . . . . . 9 ⊢ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) ∈ V
12	11	a1i 11	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) ∈ V)
13	2, 4	ushgrf 29687	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1(𝒫 𝑊 ∖ {∅}))
14		f1f1orn 6864	. . . . . . . . . . . . 13 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1(𝒫 𝑊 ∖ {∅}) → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1ontoran (iEdg‘𝐵))
15	13, 14	syl 18	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1ontoran (iEdg‘𝐵))
16		gricushgr.k	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (Edg‘𝐵)
17		edgval 29673	. . . . . . . . . . . . . 14 ⊢ (Edg‘𝐵) = ran (iEdg‘𝐵)
18	16, 17	eqtri 2786	. . . . . . . . . . . . 13 ⊢ 𝐾 = ran (iEdg‘𝐵)
19		f1oeq3 6842	. . . . . . . . . . . . 13 ⊢ (𝐾 = ran (iEdg‘𝐵) → ((iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1onto𝐾 ↔ (iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1ontoran (iEdg‘𝐵)))
20	18, 19	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1onto𝐾 ↔ (iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1ontoran (iEdg‘𝐵))
21	15, 20	sylibr 237	. . . . . . . . . . 11 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1onto𝐾)
22	21	ad3antlr 744	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1onto𝐾)
23		simprl 783	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵))
24	1, 3	ushgrf 29687	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1(𝒫 𝑉 ∖ {∅}))
25		f1f1orn 6864	. . . . . . . . . . . . . . 15 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐴))
26	24, 25	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐴))
27		gricushgr.e	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 = (Edg‘𝐴)
28		edgval 29673	. . . . . . . . . . . . . . . 16 ⊢ (Edg‘𝐴) = ran (iEdg‘𝐴)
29	27, 28	eqtri 2786	. . . . . . . . . . . . . . 15 ⊢ 𝐸 = ran (iEdg‘𝐴)
30		f1oeq3 6842	. . . . . . . . . . . . . . 15 ⊢ (𝐸 = ran (iEdg‘𝐴) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1onto𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐴)))
31	29, 30	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1onto𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐴))
32	26, 31	sylibr 237	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1onto𝐸)
33		f1ocnv 6865	. . . . . . . . . . . . 13 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1onto𝐸 → ^◡(iEdg‘𝐴):𝐸⟶1-1ontodom (iEdg‘𝐴))
34	32, 33	syl 18	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ USHGraph → ^◡(iEdg‘𝐴):𝐸⟶1-1ontodom (iEdg‘𝐴))
35	34	ad3antrrr 743	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ^◡(iEdg‘𝐴):𝐸⟶1-1ontodom (iEdg‘𝐴))
36		f1oco 6876	. . . . . . . . . . 11 ⊢ ((ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ^◡(iEdg‘𝐴):𝐸⟶1-1ontodom (iEdg‘𝐴)) → (ℎ ∘ ^◡(iEdg‘𝐴)):𝐸⟶1-1ontodom (iEdg‘𝐵))
37	23, 35, 36	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (ℎ ∘ ^◡(iEdg‘𝐴)):𝐸⟶1-1ontodom (iEdg‘𝐵))
38		f1oco 6876	. . . . . . . . . 10 ⊢ (((iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1onto𝐾 ∧ (ℎ ∘ ^◡(iEdg‘𝐴)):𝐸⟶1-1ontodom (iEdg‘𝐵)) → ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸⟶1-1onto𝐾)
39	22, 37, 38	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸⟶1-1onto𝐾)
40	29	eleq2i 2856	. . . . . . . . . . 11 ⊢ (𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ran (iEdg‘𝐴))
41		f1fn 6807	. . . . . . . . . . . . . . 15 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
42	24, 41	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
43		fvelrnb 6974	. . . . . . . . . . . . . 14 ⊢ ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
44	42, 43	syl 18	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ USHGraph → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
45	44	ad3antrrr 743	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
46		fveq2 6914	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐴)‘𝑖) = ((iEdg‘𝐴)‘𝑗))
47	46	imaeq2d 6068	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
48		2fveq3 6919	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑖 = 𝑗 → ((iEdg‘𝐵)‘(ℎ‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
49	47, 48	eqeq12d 2779	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝑗 → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
50	49	rspccv 3577	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
51	50	ad2antll 742	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))))
52	51	imp 412	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
53		coass 6288	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴)) = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))
54	53	eqcomi 2772	. . . . . . . . . . . . . . . . . . 19 ⊢ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))
55	54	fveq1i 6915	. . . . . . . . . . . . . . . . . 18 ⊢ (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)) = ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗))
56		dff1o4 6861	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐴) ↔ ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
57	26, 56	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ USHGraph → ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
58	57	simprd 501	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 ∈ USHGraph → ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴))
59	58	ad4antr 745	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴))
60		f1of 6852	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐴) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
61	26, 60	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
62	61	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
63	62	ffvelcdmda 7114	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴))
64		fvco2 7011	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((^◡(iEdg‘𝐴) Fn ran (iEdg‘𝐴) ∧ ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = (((iEdg‘𝐵) ∘ ℎ)‘(^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))))
65	59, 63, 64	syl2anc 596	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = (((iEdg‘𝐵) ∘ ℎ)‘(^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))))
66	32	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1onto𝐸)
67		f1ocnvfv1 7313	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1onto𝐸 ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
68	66, 67	sylan 592	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
69	68	fveq2d 6918	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ℎ)‘(^◡(iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))) = (((iEdg‘𝐵) ∘ ℎ)‘𝑗))
70		f1ofn 6853	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) → ℎ Fn dom (iEdg‘𝐴))
71	70	ad2antrl 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ℎ Fn dom (iEdg‘𝐴))
72		fvco2 7011	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ Fn dom (iEdg‘𝐴) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ℎ)‘𝑗) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
73	71, 72	sylan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ℎ)‘𝑗) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
74	65, 69, 73	3eqtrd 2802	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ℎ) ∘ ^◡(iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
75	55, 74	eqtr2id 2811	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐵)‘(ℎ‘𝑗)) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
76	75	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) ∧ ((iEdg‘𝐴)‘𝑗) = 𝑒) → ((iEdg‘𝐵)‘(ℎ‘𝑗)) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
77		imaeq2 6064	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑗) → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
78	77	eqcoms 2771	. . . . . . . . . . . . . . . . 17 ⊢ (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
79		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
80	78, 79	sylan9eqr 2820	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) ∧ ((iEdg‘𝐴)‘𝑗) = 𝑒) → (𝑓 “ 𝑒) = ((iEdg‘𝐵)‘(ℎ‘𝑗)))
81		fveq2 6914	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑗) → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
82	81	eqcoms 2771	. . . . . . . . . . . . . . . . 17 ⊢ (((iEdg‘𝐴)‘𝑗) = 𝑒 → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
83	82	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) ∧ ((iEdg‘𝐴)‘𝑗) = 𝑒) → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
84	76, 80, 83	3eqtr4d 2808	. . . . . . . . . . . . . . 15 ⊢ (((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) ∧ ((iEdg‘𝐴)‘𝑗) = 𝑒) → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))
85	84	ex 418	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(ℎ‘𝑗))) → (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
86	52, 85	mpdan 700	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
87	86	rexlimdva 3167	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
88	45, 87	sylbid 243	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
89	40, 88	biimtrid 245	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (𝑒 ∈ 𝐸 → (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
90	89	ralrimiv 3157	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))
91	39, 90	jca 521	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
92		f1oeq1 6840	. . . . . . . . 9 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (𝑔:𝐸⟶1-1onto𝐾 ↔ ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸⟶1-1onto𝐾))
93		fveq1 6913	. . . . . . . . . . 11 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (𝑔‘𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))
94	93	eqeq2d 2774	. . . . . . . . . 10 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
95	94	ralbidv 3189	. . . . . . . . 9 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒)))
96	92, 95	anbi12d 644	. . . . . . . 8 ⊢ (𝑔 = ((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))) → ((𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) ↔ (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴))):𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (((iEdg‘𝐵) ∘ (ℎ ∘ ^◡(iEdg‘𝐴)))‘𝑒))))
97	12, 91, 96	spcedv 3556	. . . . . . 7 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) → ∃𝑔(𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))
98	97	ex 418	. . . . . 6 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) → ((ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
99	98	exlimdv 1968	. . . . 5 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) → (∃ℎ(ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) → ∃𝑔(𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
100	6	cnvex 7969	. . . . . . . . . 10 ⊢ ^◡(iEdg‘𝐵) ∈ V
101		vex 3458	. . . . . . . . . . 11 ⊢ 𝑔 ∈ V
102	101, 8	coex 7974	. . . . . . . . . 10 ⊢ (𝑔 ∘ (iEdg‘𝐴)) ∈ V
103	100, 102	coex 7974	. . . . . . . . 9 ⊢ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V
104	103	a1i 11	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V)
105	15	ad3antlr 744	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1ontoran (iEdg‘𝐵))
106		f1ocnv 6865	. . . . . . . . . . 11 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1ontoran (iEdg‘𝐵) → ^◡(iEdg‘𝐵):ran (iEdg‘𝐵)⟶1-1ontodom (iEdg‘𝐵))
107	105, 106	syl 18	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ^◡(iEdg‘𝐵):ran (iEdg‘𝐵)⟶1-1ontodom (iEdg‘𝐵))
108		f1oeq23 6843	. . . . . . . . . . . . . 14 ⊢ ((𝐸 = ran (iEdg‘𝐴) ∧ 𝐾 = ran (iEdg‘𝐵)) → (𝑔:𝐸⟶1-1onto𝐾 ↔ 𝑔:ran (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐵)))
109	29, 18, 108	mp2an 705	. . . . . . . . . . . . 13 ⊢ (𝑔:𝐸⟶1-1onto𝐾 ↔ 𝑔:ran (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐵))
110	109	biimpi 219	. . . . . . . . . . . 12 ⊢ (𝑔:𝐸⟶1-1onto𝐾 → 𝑔:ran (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐵))
111	110	ad2antrl 741	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → 𝑔:ran (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐵))
112	26	ad3antrrr 743	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐴))
113		f1oco 6876	. . . . . . . . . . 11 ⊢ ((𝑔:ran (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐵) ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐴)) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐵))
114	111, 112, 113	syl2anc 596	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐵))
115		f1oco 6876	. . . . . . . . . 10 ⊢ ((^◡(iEdg‘𝐵):ran (iEdg‘𝐵)⟶1-1ontodom (iEdg‘𝐵) ∧ (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶1-1ontoran (iEdg‘𝐵)) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵))
116	107, 114, 115	syl2anc 596	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵))
117	61	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
118	117	ffund 6742	. . . . . . . . . . . . 13 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) → Fun (iEdg‘𝐴))
119	118	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → Fun (iEdg‘𝐴))
120		fvelrn 7106	. . . . . . . . . . . 12 ⊢ ((Fun (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
121	119, 120	sylan 592	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
122	29	raleqi 3321	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
123	122	biimpi 219	. . . . . . . . . . . . . . 15 ⊢ (∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
124	123	ad2antll 742	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
125	124	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒))
126		imaeq2 6064	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑓 “ 𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑖)))
127		fveq2 6914	. . . . . . . . . . . . . . 15 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑔‘𝑒) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
128	126, 127	eqeq12d 2779	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ((iEdg‘𝐴)‘𝑖) → ((𝑓 “ 𝑒) = (𝑔‘𝑒) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖))))
129	128	rspccva 3579	. . . . . . . . . . . . 13 ⊢ ((∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓 “ 𝑒) = (𝑔‘𝑒) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
130	125, 129	sylan 592	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
131		feq3 6717	. . . . . . . . . . . . . . . . . . . 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 237	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
134	133	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
135		f1ofn 6853	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔:𝐸⟶1-1onto𝐾 → 𝑔 Fn 𝐸)
136	135	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔 Fn 𝐸)
137	134, 136	anim12ci 626	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
138	137	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
139		fnfco 6775	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)) Fn dom (iEdg‘𝐴))
140	138, 139	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 ∘ (iEdg‘𝐴)) Fn dom (iEdg‘𝐴))
141		simplr 781	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → 𝑖 ∈ dom (iEdg‘𝐴))
142		fvco2 7011	. . . . . . . . . . . . . 14 ⊢ (((𝑔 ∘ (iEdg‘𝐴)) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
143	140, 141, 142	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
144		f1of 6852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1onto𝐾 → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
145	21, 144	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
146	145	ffund 6742	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 ∈ USHGraph → Fun (iEdg‘𝐵))
147		funcocnv2 6878	. . . . . . . . . . . . . . . . . . 19 ⊢ (Fun (iEdg‘𝐵) → ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
148	146, 147	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 ∈ USHGraph → ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
149	148	eqcomd 2769	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ USHGraph → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)))
150	149	ad5antlr 748	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)))
151	150	coeq1d 5848	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))))
152	151	fveq1d 6916	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = ((((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
153		coass 6288	. . . . . . . . . . . . . . 15 ⊢ (((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = ((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))
154	153	fveq1i 6915	. . . . . . . . . . . . . 14 ⊢ ((((iEdg‘𝐵) ∘ ^◡(iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖)
155	152, 154	eqtrdi 2814	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
156		f1of 6852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:𝐸⟶1-1onto𝐾 → 𝑔:𝐸⟶𝐾)
157		eqid 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐸 = 𝐸
158	157, 18	feq23i 6731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔:𝐸⟶𝐾 ↔ 𝑔:𝐸⟶ran (iEdg‘𝐵))
159	156, 158	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔:𝐸⟶1-1onto𝐾 → 𝑔:𝐸⟶ran (iEdg‘𝐵))
160	159	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔:𝐸⟶ran (iEdg‘𝐵))
161		f1of 6852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶1-1onto𝐸 → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
162	32, 161	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
163	162	ad2antrr 739	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
164		fco 6762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔:𝐸⟶ran (iEdg‘𝐵) ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
165	160, 163, 164	syl2anr 609	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
166	165	anim1i 627	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
167	166	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
168		ffvelcdm 7111	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵))
169	167, 168	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵))
170		fvresi 7207	. . . . . . . . . . . . . . 15 ⊢ (((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = ((𝑔 ∘ (iEdg‘𝐴))‘𝑖))
171	169, 170	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = ((𝑔 ∘ (iEdg‘𝐴))‘𝑖))
172	162	ad3antrrr 743	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
173	172	anim1i 627	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
174	173	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
175		fvco3 7014	. . . . . . . . . . . . . . 15 ⊢ (((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
176	174, 175	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
177	171, 176	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
178	143, 155, 177	3eqtr3rd 2807	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔‘((iEdg‘𝐴)‘𝑖)) = (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
179		dff1o4 6861	. . . . . . . . . . . . . . . . 17 ⊢ ((iEdg‘𝐵):dom (iEdg‘𝐵)⟶1-1onto𝐾 ↔ ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ ^◡(iEdg‘𝐵) Fn 𝐾))
180	21, 179	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ USHGraph → ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ ^◡(iEdg‘𝐵) Fn 𝐾))
181	180	simprd 501	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ USHGraph → ^◡(iEdg‘𝐵) Fn 𝐾)
182	181	ad5antlr 748	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ^◡(iEdg‘𝐵) Fn 𝐾)
183	156	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → 𝑔:𝐸⟶𝐾)
184	134, 183	anim12ci 626	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → (𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
185	184	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
186		fco 6762	. . . . . . . . . . . . . . 15 ⊢ ((𝑔:𝐸⟶𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾)
187	185, 186	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾)
188		fnfco 6775	. . . . . . . . . . . . . 14 ⊢ ((^◡(iEdg‘𝐵) Fn 𝐾 ∧ (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
189	182, 187, 188	syl2anc 596	. . . . . . . . . . . . 13 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
190		fvco2 7011	. . . . . . . . . . . . 13 ⊢ (((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
191	189, 141, 190	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
192	130, 178, 191	3eqtrd 2802	. . . . . . . . . . 11 ⊢ ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
193	121, 192	mpdan 700	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
194	193	ralrimiva 3158	. . . . . . . . 9 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
195	116, 194	jca 521	. . . . . . . 8 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
196		f1oeq1 6840	. . . . . . . . 9 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ↔ (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵)))
197		fveq1 6913	. . . . . . . . . . . 12 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (ℎ‘𝑖) = ((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
198	197	fveq2d 6918	. . . . . . . . . . 11 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((iEdg‘𝐵)‘(ℎ‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
199	198	eqeq2d 2774	. . . . . . . . . 10 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
200	199	ralbidv 3189	. . . . . . . . 9 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
201	196, 200	anbi12d 644	. . . . . . . 8 ⊢ (ℎ = (^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) ↔ ((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘((^◡(iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))))
202	104, 195, 201	spcedv 3556	. . . . . . 7 ⊢ ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) ∧ (𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))) → ∃ℎ(ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))))
203	202	ex 418	. . . . . 6 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) → ((𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))))
204	203	exlimdv 1968	. . . . 5 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) → (∃𝑔(𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)) → ∃ℎ(ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))))
205	99, 204	impbid 215	. . . 4 ⊢ (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉⟶1-1onto𝑊) → (∃ℎ(ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖))) ↔ ∃𝑔(𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒))))
206	205	pm5.32da 590	. . 3 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → ((𝑓:𝑉⟶1-1onto𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ↔ (𝑓:𝑉⟶1-1onto𝑊 ∧ ∃𝑔(𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
207	206	exbidv 1956	. 2 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (∃𝑓(𝑓:𝑉⟶1-1onto𝑊 ∧ ∃ℎ(ℎ:dom (iEdg‘𝐴)⟶1-1ontodom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(ℎ‘𝑖)))) ↔ ∃𝑓(𝑓:𝑉⟶1-1onto𝑊 ∧ ∃𝑔(𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))
208	5, 207	bitrd 282	1 ⊢ ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 ≃_𝑔𝑟 𝐵 ↔ ∃𝑓(𝑓:𝑉⟶1-1onto𝑊 ∧ ∃𝑔(𝑔:𝐸⟶1-1onto𝐾 ∧ ∀𝑒 ∈ 𝐸 (𝑓 “ 𝑒) = (𝑔‘𝑒)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∃wex 1812 ∈ wcel 2147 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ∖ cdif 4048 ∅c0 4281 𝒫 cpw 4560 {csn 4588 class class class wbr 5106 I cid 5550 ^◡ccnv 5655 dom cdm 5656 ran crn 5657 ↾ cres 5658 “ cima 5659 ∘ ccom 5660 Fun wfun 6558 Fn wfn 6559 ⟶wf 6560 ⟶1-1wf1 6561 ⟶1-1ontowf1o 6563 ‘cfv 6564 Vtxcvtx 29620 iEdgciedg 29621 Edgcedg 29671 USHGraphcushgr 29681 ≃_𝑔𝑟 cgric 49241

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-id 5551 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-ov 7452 df-oprab 7453 df-mpo 7454 df-1st 8033 df-2nd 8034 df-1o 8512 df-map 8885 df-edg 29672 df-ushgr 29683 df-grim 49243 df-gric 49246

This theorem is used by: isubgr3stgr 49340

W3C validator