Users' Mathboxes 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 43992
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.
StepHypRef Expression
1 isomushgr.v . . 3 𝑉 = (Vtx‘𝐴)
2 isomushgr.w . . 3 𝑊 = (Vtx‘𝐵)
3 eqid 2821 . . 3 (iEdg‘𝐴) = (iEdg‘𝐴)
4 eqid 2821 . . 3 (iEdg‘𝐵) = (iEdg‘𝐵)
51, 2, 3, 4isomgr 43989 . 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
98cnvex 7629 . . . . . . . . . . 11 (iEdg‘𝐴) ∈ V
107, 9coex 7634 . . . . . . . . . 10 ((iEdg‘𝐴)) ∈ V
116, 10coex 7634 . . . . . . . . 9 ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) ∈ V
1211a1i 11 . . . . . . . 8 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) ∈ V)
132, 4ushgrf 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‘𝐵))
1513, 14syl 17 . . . . . . . . . . . 12 (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵))
16 isomushgr.k . . . . . . . . . . . . . 14 𝐾 = (Edg‘𝐵)
17 edgval 26833 . . . . . . . . . . . . . 14 (Edg‘𝐵) = ran (iEdg‘𝐵)
1816, 17eqtri 2844 . . . . . . . . . . . . 13 𝐾 = ran (iEdg‘𝐵)
19 f1oeq3 6605 . . . . . . . . . . . . 13 (𝐾 = ran (iEdg‘𝐵) → ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto𝐾 ↔ (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵)))
2018, 19ax-mp 5 . . . . . . . . . . . 12 ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto𝐾 ↔ (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵))
2115, 20sylibr 236 . . . . . . . . . . 11 (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto𝐾)
2221ad3antlr 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‘𝐵))
241, 3ushgrf 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‘𝐴))
2624, 25syl 17 . . . . . . . . . . . . . 14 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴))
27 isomushgr.e . . . . . . . . . . . . . . . 16 𝐸 = (Edg‘𝐴)
28 edgval 26833 . . . . . . . . . . . . . . . 16 (Edg‘𝐴) = ran (iEdg‘𝐴)
2927, 28eqtri 2844 . . . . . . . . . . . . . . 15 𝐸 = ran (iEdg‘𝐴)
30 f1oeq3 6605 . . . . . . . . . . . . . . 15 (𝐸 = ran (iEdg‘𝐴) → ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴)))
3129, 30ax-mp 5 . . . . . . . . . . . . . 14 ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴))
3226, 31sylibr 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‘𝐴))
3432, 33syl 17 . . . . . . . . . . . 12 (𝐴 ∈ USHGraph → (iEdg‘𝐴):𝐸1-1-onto→dom (iEdg‘𝐴))
3534ad3antrrr 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‘𝐵))
3723, 35, 36syl2anc 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𝐾)
3922, 37, 38syl2anc 586 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾)
4029eleq2i 2904 . . . . . . . . . . 11 (𝑒𝐸𝑒 ∈ ran (iEdg‘𝐴))
41 f1fn 6575 . . . . . . . . . . . . . . 15 ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
4224, 41syl 17 . . . . . . . . . . . . . 14 (𝐴 ∈ USHGraph → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
43 fvelrnb 6725 . . . . . . . . . . . . . 14 ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
4442, 43syl 17 . . . . . . . . . . . . 13 (𝐴 ∈ USHGraph → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
4544ad3antrrr 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‘𝐴)‘𝑗))
4746imaeq2d 5928 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
48 2fveq3 6674 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((iEdg‘𝐵)‘(𝑖)) = ((iEdg‘𝐵)‘(𝑗)))
4947, 48eqeq12d 2837 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗))))
5049rspccv 3619 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗))))
5150ad2antll 727 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗))))
5251imp 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‘𝐴)))
5453eqcomi 2830 . . . . . . . . . . . . . . . . . . 19 ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴))
5554fveq1i 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‘𝐴)))
5726, 56sylib 220 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ USHGraph → ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ (iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
5857simprd 498 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ USHGraph → (iEdg‘𝐴) Fn ran (iEdg‘𝐴))
5958ad4antr 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‘𝐴))
6126, 60syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
6261ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
6362ffvelrnda 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‘𝐴)‘𝑗))))
6559, 63, 64syl2anc 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‘𝐴)‘𝑗))))
6632ad3antrrr 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‘𝐴)‘𝑗)) = 𝑗)
6866, 67sylan 582 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
6968fveq2d 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‘𝐴))
7170ad2antrl 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‘𝐵)‘(𝑗)))
7371, 72sylan 582 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ )‘𝑗) = ((iEdg‘𝐵)‘(𝑗)))
7465, 69, 733eqtrd 2860 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗)))
7555, 74syl5req 2869 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐵)‘(𝑗)) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
7675ad2antrr 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‘𝐴)‘𝑗)))
7877eqcoms 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‘𝐵)‘(𝑗)))
8078, 79sylan9eqr 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‘𝐴)‘𝑗)))
8281eqcoms 2829 . . . . . . . . . . . . . . . . 17 (((iEdg‘𝐴)‘𝑗) = 𝑒 → (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
8382adantl 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‘𝐴)‘𝑗)))
8476, 80, 833eqtr4d 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‘𝐴)))‘𝑒))
8584ex 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‘𝐴)))‘𝑒)))
8652, 85mpdan 685 . . . . . . . . . . . . 13 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
8786rexlimdva 3284 . . . . . . . . . . . 12 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
8845, 87sylbid 242 . . . . . . . . . . 11 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
8940, 88syl5bi 244 . . . . . . . . . 10 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (𝑒𝐸 → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
9089ralrimiv 3181 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ∀𝑒𝐸 (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒))
9139, 90jca 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‘𝐴)))‘𝑒))
9493eqeq2d 2832 . . . . . . . . . 10 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → ((𝑓𝑒) = (𝑔𝑒) ↔ (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
9594ralbidv 3197 . . . . . . . . 9 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → (∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒) ↔ ∀𝑒𝐸 (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
9692, 95anbi12d 632 . . . . . . . 8 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) ↔ (((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒))))
9712, 91, 96spcedv 3598 . . . . . . 7 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)))
9897ex 415 . . . . . 6 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → ((:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))) → ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))))
9998exlimdv 1930 . . . . 5 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))) → ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))))
1006cnvex 7629 . . . . . . . . . 10 (iEdg‘𝐵) ∈ V
101 vex 3497 . . . . . . . . . . 11 𝑔 ∈ V
102101, 8coex 7634 . . . . . . . . . 10 (𝑔 ∘ (iEdg‘𝐴)) ∈ V
103100, 102coex 7634 . . . . . . . . 9 ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V
104103a1i 11 . . . . . . . 8 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V)
10515ad3antlr 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‘𝐵))
107105, 106syl 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‘𝐵)))
10929, 18, 108mp2an 690 . . . . . . . . . . . . 13 (𝑔:𝐸1-1-onto𝐾𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
110109biimpi 218 . . . . . . . . . . . 12 (𝑔:𝐸1-1-onto𝐾𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
111110ad2antrl 726 . . . . . . . . . . 11 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
11226ad3antrrr 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‘𝐵))
114111, 112, 113syl2anc 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‘𝐵))
116107, 114, 115syl2anc 586 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵))
11761ad2antrr 724 . . . . . . . . . . . . . 14 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
118117ffund 6517 . . . . . . . . . . . . 13 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → Fun (iEdg‘𝐴))
119118adantr 483 . . . . . . . . . . . 12 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → Fun (iEdg‘𝐴))
120 fvelrn 6843 . . . . . . . . . . . 12 ((Fun (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
121119, 120sylan 582 . . . . . . . . . . 11 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
12229raleqi 3413 . . . . . . . . . . . . . . . 16 (∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒) ↔ ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
123122biimpi 218 . . . . . . . . . . . . . . 15 (∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
124123ad2antll 727 . . . . . . . . . . . . . 14 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
125124adantr 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‘𝐴)‘𝑖)))
128126, 127eqeq12d 2837 . . . . . . . . . . . . . 14 (𝑒 = ((iEdg‘𝐴)‘𝑖) → ((𝑓𝑒) = (𝑔𝑒) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖))))
129128rspccva 3621 . . . . . . . . . . . . 13 ((∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
130125, 129sylan 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‘𝐴)))
13229, 131ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
13361, 132sylibr 236 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
134133ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
135 f1ofn 6615 . . . . . . . . . . . . . . . . . 18 (𝑔:𝐸1-1-onto𝐾𝑔 Fn 𝐸)
136135adantr 483 . . . . . . . . . . . . . . . . 17 ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → 𝑔 Fn 𝐸)
137134, 136anim12ci 615 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
138137ad2antrr 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‘𝐴))
140138, 139syl 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‘𝐴))
142141adantr 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‘𝐴))‘𝑖)))
144140, 142, 143syl2anc 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‘𝐵)⟶𝐾)
14621, 145syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
147146ffund 6517 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ USHGraph → Fun (iEdg‘𝐵))
148 funcocnv2 6638 . . . . . . . . . . . . . . . . . . 19 (Fun (iEdg‘𝐵) → ((iEdg‘𝐵) ∘ (iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
149147, 148syl 17 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ USHGraph → ((iEdg‘𝐵) ∘ (iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
150149eqcomd 2827 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ USHGraph → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ (iEdg‘𝐵)))
151150ad5antlr 733 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ (iEdg‘𝐵)))
152151coeq1d 5731 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))))
153152fveq1d 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‘𝐴))))
155154fveq1i 6670 . . . . . . . . . . . . . 14 ((((iEdg‘𝐵) ∘ (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖)
156153, 155syl6eq 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 𝐸 = 𝐸
159158, 18feq23i 6507 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:𝐸𝐾𝑔:𝐸⟶ran (iEdg‘𝐵))
160157, 159sylib 220 . . . . . . . . . . . . . . . . . . . 20 (𝑔:𝐸1-1-onto𝐾𝑔:𝐸⟶ran (iEdg‘𝐵))
161160adantr 483 . . . . . . . . . . . . . . . . . . 19 ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → 𝑔:𝐸⟶ran (iEdg‘𝐵))
162 f1of 6614 . . . . . . . . . . . . . . . . . . . . 21 ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto𝐸 → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
16332, 162syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
164163ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
165 fco 6530 . . . . . . . . . . . . . . . . . . 19 ((𝑔:𝐸⟶ran (iEdg‘𝐵) ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
166161, 164, 165syl2anr 598 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
167166anim1i 616 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
168167adantr 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‘𝐵))
170168, 169syl 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‘𝐴))‘𝑖))
172170, 171syl 17 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = ((𝑔 ∘ (iEdg‘𝐴))‘𝑖))
173163ad3antrrr 728 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
174173anim1i 616 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸𝑖 ∈ dom (iEdg‘𝐴)))
175174adantr 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‘𝐴)‘𝑖)))
177175, 176syl 17 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
178172, 177eqtrd 2856 . . . . . . . . . . . . 13 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
179144, 156, 1783eqtr3rd 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 𝐾))
18121, 180sylib 220 . . . . . . . . . . . . . . . 16 (𝐵 ∈ USHGraph → ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ (iEdg‘𝐵) Fn 𝐾))
182181simprd 498 . . . . . . . . . . . . . . 15 (𝐵 ∈ USHGraph → (iEdg‘𝐵) Fn 𝐾)
183182ad5antlr 733 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (iEdg‘𝐵) Fn 𝐾)
184157adantr 483 . . . . . . . . . . . . . . . . 17 ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → 𝑔:𝐸𝐾)
185134, 184anim12ci 615 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (𝑔:𝐸𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
186185ad2antrr 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‘𝐴)⟶𝐾)
188186, 187syl 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‘𝐴))
190183, 188, 189syl2anc 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‘𝐴)))‘𝑖)))
192190, 142, 191syl2anc 586 . . . . . . . . . . . 12 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
193130, 179, 1923eqtrd 2860 . . . . . . . . . . 11 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
194121, 193mpdan 685 . . . . . . . . . 10 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
195194ralrimiva 3182 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
196116, 195jca 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‘𝐴)))‘𝑖))
199198fveq2d 6673 . . . . . . . . . . 11 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((iEdg‘𝐵)‘(𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
200199eqeq2d 2832 . . . . . . . . . 10 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
201200ralbidv 3197 . . . . . . . . 9 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
202197, 201anbi12d 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‘𝐴)))‘𝑖)))))
203104, 196, 202spcedv 3598 . . . . . . 7 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))))
204203ex 415 . . . . . 6 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))))
205204exlimdv 1930 . . . . 5 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))))
20699, 205impbid 214 . . . 4 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))) ↔ ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))))
207206pm5.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𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)))))
208207exbidv 1918 . 2 ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (∃𝑓(𝑓:𝑉1-1-onto𝑊 ∧ ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ↔ ∃𝑓(𝑓:𝑉1-1-onto𝑊 ∧ ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)))))
2095, 208bitrd 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-1wf1 6351  1-1-ontowf1o 6353  cfv 6354  Vtxcvtx 26780  iEdgciedg 26781  Edgcedg 26831  USHGraphcushgr 26841   IsomGr cisomgr 43985
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 43987
This theorem is referenced by:  isomuspgr  44000
  Copyright terms: Public domain W3C validator