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 46573
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 2732 . . 3 (iEdg‘𝐴) = (iEdg‘𝐴)
4 eqid 2732 . . 3 (iEdg‘𝐵) = (iEdg‘𝐵)
51, 2, 3, 4isomgr 46570 . 2 ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:𝑉1-1-onto𝑊 ∧ ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))))))
6 fvex 6904 . . . . . . . . . 10 (iEdg‘𝐵) ∈ V
7 vex 3478 . . . . . . . . . . 11 ∈ V
8 fvex 6904 . . . . . . . . . . . 12 (iEdg‘𝐴) ∈ V
98cnvex 7918 . . . . . . . . . . 11 (iEdg‘𝐴) ∈ V
107, 9coex 7923 . . . . . . . . . 10 ((iEdg‘𝐴)) ∈ V
116, 10coex 7923 . . . . . . . . 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 28361 . . . . . . . . . . . . 13 (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1→(𝒫 𝑊 ∖ {∅}))
14 f1f1orn 6844 . . . . . . . . . . . . 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 28347 . . . . . . . . . . . . . 14 (Edg‘𝐵) = ran (iEdg‘𝐵)
1816, 17eqtri 2760 . . . . . . . . . . . . 13 𝐾 = ran (iEdg‘𝐵)
19 f1oeq3 6823 . . . . . . . . . . . . 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 233 . . . . . . . . . . 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 28361 . . . . . . . . . . . . . . 15 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}))
25 f1f1orn 6844 . . . . . . . . . . . . . . 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 28347 . . . . . . . . . . . . . . . 16 (Edg‘𝐴) = ran (iEdg‘𝐴)
2927, 28eqtri 2760 . . . . . . . . . . . . . . 15 𝐸 = ran (iEdg‘𝐴)
30 f1oeq3 6823 . . . . . . . . . . . . . . 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 233 . . . . . . . . . . . . 13 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto𝐸)
33 f1ocnv 6845 . . . . . . . . . . . . 13 ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto𝐸(iEdg‘𝐴):𝐸1-1-onto→dom (iEdg‘𝐴))
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 6856 . . . . . . . . . . 11 ((:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ (iEdg‘𝐴):𝐸1-1-onto→dom (iEdg‘𝐴)) → ((iEdg‘𝐴)):𝐸1-1-onto→dom (iEdg‘𝐵))
3723, 35, 36syl2anc 584 . . . . . . . . . 10 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ((iEdg‘𝐴)):𝐸1-1-onto→dom (iEdg‘𝐵))
38 f1oco 6856 . . . . . . . . . 10 (((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto𝐾 ∧ ((iEdg‘𝐴)):𝐸1-1-onto→dom (iEdg‘𝐵)) → ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾)
3922, 37, 38syl2anc 584 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾)
4029eleq2i 2825 . . . . . . . . . . 11 (𝑒𝐸𝑒 ∈ ran (iEdg‘𝐴))
41 f1fn 6788 . . . . . . . . . . . . . . 15 ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
4224, 41syl 17 . . . . . . . . . . . . . 14 (𝐴 ∈ USHGraph → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
43 fvelrnb 6952 . . . . . . . . . . . . . 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 6891 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → ((iEdg‘𝐴)‘𝑖) = ((iEdg‘𝐴)‘𝑗))
4746imaeq2d 6059 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
48 2fveq3 6896 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((iEdg‘𝐵)‘(𝑖)) = ((iEdg‘𝐵)‘(𝑗)))
4947, 48eqeq12d 2748 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗))))
5049rspccv 3609 . . . . . . . . . . . . . . . 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 407 . . . . . . . . . . . . . 14 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗)))
53 coass 6264 . . . . . . . . . . . . . . . . . . . 20 (((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴)) = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))
5453eqcomi 2741 . . . . . . . . . . . . . . . . . . 19 ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴))
5554fveq1i 6892 . . . . . . . . . . . . . . . . . 18 (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)) = ((((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗))
56 dff1o4 6841 . . . . . . . . . . . . . . . . . . . . . . 23 ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴) ↔ ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ (iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
5726, 56sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ USHGraph → ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ (iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
5857simprd 496 . . . . . . . . . . . . . . . . . . . . 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 6833 . . . . . . . . . . . . . . . . . . . . . . 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‘𝐴))
6362ffvelcdmda 7086 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴))
64 fvco2 6988 . . . . . . . . . . . . . . . . . . . 20 (((iEdg‘𝐴) Fn ran (iEdg‘𝐴) ∧ ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = (((iEdg‘𝐵) ∘ )‘((iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))))
6559, 63, 64syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = (((iEdg‘𝐵) ∘ )‘((iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))))
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 7276 . . . . . . . . . . . . . . . . . . . . 21 (((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto𝐸𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
6866, 67sylan 580 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
6968fveq2d 6895 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ )‘((iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))) = (((iEdg‘𝐵) ∘ )‘𝑗))
70 f1ofn 6834 . . . . . . . . . . . . . . . . . . . . 21 (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) → Fn dom (iEdg‘𝐴))
7170ad2antrl 726 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → Fn dom (iEdg‘𝐴))
72 fvco2 6988 . . . . . . . . . . . . . . . . . . . 20 (( Fn dom (iEdg‘𝐴) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ )‘𝑗) = ((iEdg‘𝐵)‘(𝑗)))
7371, 72sylan 580 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ )‘𝑗) = ((iEdg‘𝐵)‘(𝑗)))
7465, 69, 733eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗)))
7555, 74eqtr2id 2785 . . . . . . . . . . . . . . . . 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 6055 . . . . . . . . . . . . . . . . . 18 (𝑒 = ((iEdg‘𝐴)‘𝑗) → (𝑓𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
7877eqcoms 2740 . . . . . . . . . . . . . . . . 17 (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
79 simpr 485 . . . . . . . . . . . . . . . . 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 2794 . . . . . . . . . . . . . . . 16 (((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) ∧ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗))) ∧ ((iEdg‘𝐴)‘𝑗) = 𝑒) → (𝑓𝑒) = ((iEdg‘𝐵)‘(𝑗)))
81 fveq2 6891 . . . . . . . . . . . . . . . . . 18 (𝑒 = ((iEdg‘𝐴)‘𝑗) → (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
8281eqcoms 2740 . . . . . . . . . . . . . . . . 17 (((iEdg‘𝐴)‘𝑗) = 𝑒 → (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
8382adantl 482 . . . . . . . . . . . . . . . 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 2782 . . . . . . . . . . . . . . 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 413 . . . . . . . . . . . . . 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 3155 . . . . . . . . . . . 12 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
8845, 87sylbid 239 . . . . . . . . . . 11 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
8940, 88biimtrid 241 . . . . . . . . . 10 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (𝑒𝐸 → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
9089ralrimiv 3145 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ∀𝑒𝐸 (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒))
9139, 90jca 512 . . . . . . . 8 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
92 f1oeq1 6821 . . . . . . . . 9 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → (𝑔:𝐸1-1-onto𝐾 ↔ ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾))
93 fveq1 6890 . . . . . . . . . . 11 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → (𝑔𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒))
9493eqeq2d 2743 . . . . . . . . . 10 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → ((𝑓𝑒) = (𝑔𝑒) ↔ (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
9594ralbidv 3177 . . . . . . . . 9 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → (∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒) ↔ ∀𝑒𝐸 (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
9692, 95anbi12d 631 . . . . . . . 8 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) ↔ (((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒))))
9712, 91, 96spcedv 3588 . . . . . . 7 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)))
9897ex 413 . . . . . 6 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → ((:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))) → ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))))
9998exlimdv 1936 . . . . 5 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))) → ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))))
1006cnvex 7918 . . . . . . . . . 10 (iEdg‘𝐵) ∈ V
101 vex 3478 . . . . . . . . . . 11 𝑔 ∈ V
102101, 8coex 7923 . . . . . . . . . 10 (𝑔 ∘ (iEdg‘𝐴)) ∈ V
103100, 102coex 7923 . . . . . . . . 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 6845 . . . . . . . . . . 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 6824 . . . . . . . . . . . . . 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 215 . . . . . . . . . . . 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 6856 . . . . . . . . . . 11 ((𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵) ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴)) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
114111, 112, 113syl2anc 584 . . . . . . . . . 10 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
115 f1oco 6856 . . . . . . . . . 10 (((iEdg‘𝐵):ran (iEdg‘𝐵)–1-1-onto→dom (iEdg‘𝐵) ∧ (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵)) → ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵))
116107, 114, 115syl2anc 584 . . . . . . . . 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 6721 . . . . . . . . . . . . 13 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → Fun (iEdg‘𝐴))
119118adantr 481 . . . . . . . . . . . 12 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → Fun (iEdg‘𝐴))
120 fvelrn 7078 . . . . . . . . . . . 12 ((Fun (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
121119, 120sylan 580 . . . . . . . . . . 11 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
12229raleqi 3323 . . . . . . . . . . . . . . . 16 (∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒) ↔ ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
123122biimpi 215 . . . . . . . . . . . . . . 15 (∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
124123ad2antll 727 . . . . . . . . . . . . . 14 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
125124adantr 481 . . . . . . . . . . . . 13 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
126 imaeq2 6055 . . . . . . . . . . . . . . 15 (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑓𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑖)))
127 fveq2 6891 . . . . . . . . . . . . . . 15 (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑔𝑒) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
128126, 127eqeq12d 2748 . . . . . . . . . . . . . 14 (𝑒 = ((iEdg‘𝐴)‘𝑖) → ((𝑓𝑒) = (𝑔𝑒) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖))))
129128rspccva 3611 . . . . . . . . . . . . 13 ((∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
130125, 129sylan 580 . . . . . . . . . . . 12 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
131 feq3 6700 . . . . . . . . . . . . . . . . . . . 20 (𝐸 = ran (iEdg‘𝐴) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴)))
13229, 131ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸 ↔ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
13361, 132sylibr 233 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
134133ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
135 f1ofn 6834 . . . . . . . . . . . . . . . . . 18 (𝑔:𝐸1-1-onto𝐾𝑔 Fn 𝐸)
136135adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → 𝑔 Fn 𝐸)
137134, 136anim12ci 614 . . . . . . . . . . . . . . . 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 6756 . . . . . . . . . . . . . . 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 simplr 767 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → 𝑖 ∈ dom (iEdg‘𝐴))
142 fvco2 6988 . . . . . . . . . . . . . 14 (((𝑔 ∘ (iEdg‘𝐴)) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
143140, 141, 142syl2anc 584 . . . . . . . . . . . . 13 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
144 f1of 6833 . . . . . . . . . . . . . . . . . . . . 21 ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto𝐾 → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
14521, 144syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
146145ffund 6721 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ USHGraph → Fun (iEdg‘𝐵))
147 funcocnv2 6858 . . . . . . . . . . . . . . . . . . 19 (Fun (iEdg‘𝐵) → ((iEdg‘𝐵) ∘ (iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
148146, 147syl 17 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ USHGraph → ((iEdg‘𝐵) ∘ (iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
149148eqcomd 2738 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ USHGraph → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ (iEdg‘𝐵)))
150149ad5antlr 733 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ (iEdg‘𝐵)))
151150coeq1d 5861 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))))
152151fveq1d 6893 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = ((((iEdg‘𝐵) ∘ (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
153 coass 6264 . . . . . . . . . . . . . . 15 (((iEdg‘𝐵) ∘ (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = ((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))
154153fveq1i 6892 . . . . . . . . . . . . . 14 ((((iEdg‘𝐵) ∘ (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖)
155152, 154eqtrdi 2788 . . . . . . . . . . . . 13 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
156 f1of 6833 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:𝐸1-1-onto𝐾𝑔:𝐸𝐾)
157 eqid 2732 . . . . . . . . . . . . . . . . . . . . . 22 𝐸 = 𝐸
158157, 18feq23i 6711 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:𝐸𝐾𝑔:𝐸⟶ran (iEdg‘𝐵))
159156, 158sylib 217 . . . . . . . . . . . . . . . . . . . 20 (𝑔:𝐸1-1-onto𝐾𝑔:𝐸⟶ran (iEdg‘𝐵))
160159adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → 𝑔:𝐸⟶ran (iEdg‘𝐵))
161 f1of 6833 . . . . . . . . . . . . . . . . . . . . 21 ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto𝐸 → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
16232, 161syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
163162ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
164 fco 6741 . . . . . . . . . . . . . . . . . . 19 ((𝑔:𝐸⟶ran (iEdg‘𝐵) ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
165160, 163, 164syl2anr 597 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
166165anim1i 615 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
167166adantr 481 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
168 ffvelcdm 7083 . . . . . . . . . . . . . . . 16 (((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵))
169167, 168syl 17 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵))
170 fvresi 7173 . . . . . . . . . . . . . . 15 (((𝑔 ∘ (iEdg‘𝐴))‘𝑖) ∈ ran (iEdg‘𝐵) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = ((𝑔 ∘ (iEdg‘𝐴))‘𝑖))
171169, 170syl 17 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = ((𝑔 ∘ (iEdg‘𝐴))‘𝑖))
172162ad3antrrr 728 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
173172anim1i 615 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸𝑖 ∈ dom (iEdg‘𝐴)))
174173adantr 481 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸𝑖 ∈ dom (iEdg‘𝐴)))
175 fvco3 6990 . . . . . . . . . . . . . . 15 (((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
176174, 175syl 17 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴))‘𝑖) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
177171, 176eqtrd 2772 . . . . . . . . . . . . 13 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
178143, 155, 1773eqtr3rd 2781 . . . . . . . . . . . 12 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔‘((iEdg‘𝐴)‘𝑖)) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
179 dff1o4 6841 . . . . . . . . . . . . . . . . 17 ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto𝐾 ↔ ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ (iEdg‘𝐵) Fn 𝐾))
18021, 179sylib 217 . . . . . . . . . . . . . . . 16 (𝐵 ∈ USHGraph → ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ (iEdg‘𝐵) Fn 𝐾))
181180simprd 496 . . . . . . . . . . . . . . 15 (𝐵 ∈ USHGraph → (iEdg‘𝐵) Fn 𝐾)
182181ad5antlr 733 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (iEdg‘𝐵) Fn 𝐾)
183156adantr 481 . . . . . . . . . . . . . . . . 17 ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → 𝑔:𝐸𝐾)
184134, 183anim12ci 614 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (𝑔:𝐸𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
185184ad2antrr 724 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔:𝐸𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
186 fco 6741 . . . . . . . . . . . . . . 15 ((𝑔:𝐸𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾)
187185, 186syl 17 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾)
188 fnfco 6756 . . . . . . . . . . . . . 14 (((iEdg‘𝐵) Fn 𝐾 ∧ (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾) → ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
189182, 187, 188syl2anc 584 . . . . . . . . . . . . 13 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
190 fvco2 6988 . . . . . . . . . . . . 13 ((((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
191189, 141, 190syl2anc 584 . . . . . . . . . . . 12 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
192130, 178, 1913eqtrd 2776 . . . . . . . . . . 11 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
193121, 192mpdan 685 . . . . . . . . . 10 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
194193ralrimiva 3146 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
195116, 194jca 512 . . . . . . . 8 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
196 f1oeq1 6821 . . . . . . . . 9 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ↔ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵)))
197 fveq1 6890 . . . . . . . . . . . 12 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (𝑖) = (((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
198197fveq2d 6895 . . . . . . . . . . 11 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((iEdg‘𝐵)‘(𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
199198eqeq2d 2743 . . . . . . . . . 10 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
200199ralbidv 3177 . . . . . . . . 9 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
201196, 200anbi12d 631 . . . . . . . 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‘𝐴)))‘𝑖)))))
202104, 195, 201spcedv 3588 . . . . . . 7 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))))
203202ex 413 . . . . . 6 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))))
204203exlimdv 1936 . . . . 5 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))))
20599, 204impbid 211 . . . 4 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))) ↔ ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))))
206205pm5.32da 579 . . 3 ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → ((𝑓:𝑉1-1-onto𝑊 ∧ ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ↔ (𝑓:𝑉1-1-onto𝑊 ∧ ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)))))
207206exbidv 1924 . 2 ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (∃𝑓(𝑓:𝑉1-1-onto𝑊 ∧ ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ↔ ∃𝑓(𝑓:𝑉1-1-onto𝑊 ∧ ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)))))
2085, 207bitrd 278 1 ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:𝑉1-1-onto𝑊 ∧ ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  wral 3061  wrex 3070  Vcvv 3474  cdif 3945  c0 4322  𝒫 cpw 4602  {csn 4628   class class class wbr 5148   I cid 5573  ccnv 5675  dom cdm 5676  ran crn 5677  cres 5678  cima 5679  ccom 5680  Fun wfun 6537   Fn wfn 6538  wf 6539  1-1wf1 6540  1-1-ontowf1o 6542  cfv 6543  Vtxcvtx 28294  iEdgciedg 28295  Edgcedg 28345  USHGraphcushgr 28355   IsomGr cisomgr 46566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-edg 28346  df-ushgr 28357  df-isomgr 46568
This theorem is referenced by:  isomuspgr  46581
  Copyright terms: Public domain W3C validator