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 42562
 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 2825 . . 3 (iEdg‘𝐴) = (iEdg‘𝐴)
4 eqid 2825 . . 3 (iEdg‘𝐵) = (iEdg‘𝐵)
51, 2, 3, 4isomgr 42559 . 2 ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:𝑉1-1-onto𝑊 ∧ ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))))))
6 fvex 6450 . . . . . . . . . 10 (iEdg‘𝐵) ∈ V
7 vex 3417 . . . . . . . . . . 11 ∈ V
8 fvex 6450 . . . . . . . . . . . 12 (iEdg‘𝐴) ∈ V
98cnvex 7380 . . . . . . . . . . 11 (iEdg‘𝐴) ∈ V
107, 9coex 7385 . . . . . . . . . 10 ((iEdg‘𝐴)) ∈ V
116, 10coex 7385 . . . . . . . . 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 26368 . . . . . . . . . . . . 13 (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1→(𝒫 𝑊 ∖ {∅}))
14 f1f1orn 6393 . . . . . . . . . . . . 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 26354 . . . . . . . . . . . . . 14 (Edg‘𝐵) = ran (iEdg‘𝐵)
1816, 17eqtri 2849 . . . . . . . . . . . . 13 𝐾 = ran (iEdg‘𝐵)
19 f1oeq3 6373 . . . . . . . . . . . . 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 226 . . . . . . . . . . 11 (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto𝐾)
2221ad3antlr 722 . . . . . . . . . 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 787 . . . . . . . . . . 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 26368 . . . . . . . . . . . . . . 15 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}))
25 f1f1orn 6393 . . . . . . . . . . . . . . 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 26354 . . . . . . . . . . . . . . . 16 (Edg‘𝐴) = ran (iEdg‘𝐴)
2927, 28eqtri 2849 . . . . . . . . . . . . . . 15 𝐸 = ran (iEdg‘𝐴)
30 f1oeq3 6373 . . . . . . . . . . . . . . 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 226 . . . . . . . . . . . . 13 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto𝐸)
33 f1ocnv 6394 . . . . . . . . . . . . 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 721 . . . . . . . . . . 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 6404 . . . . . . . . . . 11 ((:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ (iEdg‘𝐴):𝐸1-1-onto→dom (iEdg‘𝐴)) → ((iEdg‘𝐴)):𝐸1-1-onto→dom (iEdg‘𝐵))
3723, 35, 36syl2anc 579 . . . . . . . . . 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 6404 . . . . . . . . . 10 (((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto𝐾 ∧ ((iEdg‘𝐴)):𝐸1-1-onto→dom (iEdg‘𝐵)) → ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾)
3922, 37, 38syl2anc 579 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾)
4029eleq2i 2898 . . . . . . . . . . 11 (𝑒𝐸𝑒 ∈ ran (iEdg‘𝐴))
41 f1fn 6343 . . . . . . . . . . . . . . 15 ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1→(𝒫 𝑉 ∖ {∅}) → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
4224, 41syl 17 . . . . . . . . . . . . . 14 (𝐴 ∈ USHGraph → (iEdg‘𝐴) Fn dom (iEdg‘𝐴))
43 fvelrnb 6494 . . . . . . . . . . . . . 14 ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
4442, 43syl 17 . . . . . . . . . . . . 13 (𝐴 ∈ USHGraph → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
4544ad3antrrr 721 . . . . . . . . . . . 12 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) ↔ ∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒))
46 fveq2 6437 . . . . . . . . . . . . . . . . . . 19 (𝑖 = 𝑗 → ((iEdg‘𝐴)‘𝑖) = ((iEdg‘𝐴)‘𝑗))
4746imaeq2d 5711 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
48 2fveq3 6442 . . . . . . . . . . . . . . . . . 18 (𝑖 = 𝑗 → ((iEdg‘𝐵)‘(𝑖)) = ((iEdg‘𝐵)‘(𝑗)))
4947, 48eqeq12d 2840 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝑗 → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗))))
5049rspccv 3523 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗))))
5150ad2antll 720 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (𝑗 ∈ dom (iEdg‘𝐴) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗))))
5251imp 397 . . . . . . . . . . . . . 14 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑗)) = ((iEdg‘𝐵)‘(𝑗)))
53 coass 5899 . . . . . . . . . . . . . . . . . . . 20 (((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴)) = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))
5453eqcomi 2834 . . . . . . . . . . . . . . . . . . 19 ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴))
5554fveq1i 6438 . . . . . . . . . . . . . . . . . 18 (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)) = ((((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗))
56 dff1o4 6390 . . . . . . . . . . . . . . . . . . . . . . 23 ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴) ↔ ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ (iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
5726, 56sylib 210 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴 ∈ USHGraph → ((iEdg‘𝐴) Fn dom (iEdg‘𝐴) ∧ (iEdg‘𝐴) Fn ran (iEdg‘𝐴)))
5857simprd 491 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 ∈ USHGraph → (iEdg‘𝐴) Fn ran (iEdg‘𝐴))
5958ad4antr 724 . . . . . . . . . . . . . . . . . . . 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 6382 . . . . . . . . . . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
6362ffvelrnda 6613 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴))
64 fvco2 6524 . . . . . . . . . . . . . . . . . . . 20 (((iEdg‘𝐴) Fn ran (iEdg‘𝐴) ∧ ((iEdg‘𝐴)‘𝑗) ∈ ran (iEdg‘𝐴)) → ((((iEdg‘𝐵) ∘ ) ∘ (iEdg‘𝐴))‘((iEdg‘𝐴)‘𝑗)) = (((iEdg‘𝐵) ∘ )‘((iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗))))
6559, 63, 64syl2anc 579 . . . . . . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . . . . . . . . . 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 6792 . . . . . . . . . . . . . . . . . . . . 21 (((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto𝐸𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
6866, 67sylan 575 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘((iEdg‘𝐴)‘𝑗)) = 𝑗)
6968fveq2d 6441 . . . . . . . . . . . . . . . . . . 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 6383 . . . . . . . . . . . . . . . . . . . . 21 (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) → Fn dom (iEdg‘𝐴))
7170ad2antrl 719 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → Fn dom (iEdg‘𝐴))
72 fvco2 6524 . . . . . . . . . . . . . . . . . . . 20 (( Fn dom (iEdg‘𝐴) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ )‘𝑗) = ((iEdg‘𝐵)‘(𝑗)))
7371, 72sylan 575 . . . . . . . . . . . . . . . . . . 19 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ )‘𝑗) = ((iEdg‘𝐵)‘(𝑗)))
7465, 69, 733eqtrd 2865 . . . . . . . . . . . . . . . . . 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 2874 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐵)‘(𝑗)) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
7675ad2antrr 717 . . . . . . . . . . . . . . . 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 5707 . . . . . . . . . . . . . . . . . 18 (𝑒 = ((iEdg‘𝐴)‘𝑗) → (𝑓𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
7877eqcoms 2833 . . . . . . . . . . . . . . . . 17 (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑗)))
79 simpr 479 . . . . . . . . . . . . . . . . 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 2883 . . . . . . . . . . . . . . . 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 6437 . . . . . . . . . . . . . . . . . 18 (𝑒 = ((iEdg‘𝐴)‘𝑗) → (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
8281eqcoms 2833 . . . . . . . . . . . . . . . . 17 (((iEdg‘𝐴)‘𝑗) = 𝑒 → (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘((iEdg‘𝐴)‘𝑗)))
8382adantl 475 . . . . . . . . . . . . . . . 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 2871 . . . . . . . . . . . . . . 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 403 . . . . . . . . . . . . . 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 678 . . . . . . . . . . . . 13 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ∧ 𝑗 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
8786rexlimdva 3240 . . . . . . . . . . . 12 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (∃𝑗 ∈ dom (iEdg‘𝐴)((iEdg‘𝐴)‘𝑗) = 𝑒 → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
8845, 87sylbid 232 . . . . . . . . . . 11 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (𝑒 ∈ ran (iEdg‘𝐴) → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
8940, 88syl5bi 234 . . . . . . . . . 10 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → (𝑒𝐸 → (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
9089ralrimiv 3174 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ∀𝑒𝐸 (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒))
9139, 90jca 507 . . . . . . . 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 6371 . . . . . . . . 9 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → (𝑔:𝐸1-1-onto𝐾 ↔ ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾))
93 fveq1 6436 . . . . . . . . . . 11 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → (𝑔𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒))
9493eqeq2d 2835 . . . . . . . . . 10 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → ((𝑓𝑒) = (𝑔𝑒) ↔ (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
9594ralbidv 3195 . . . . . . . . 9 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → (∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒) ↔ ∀𝑒𝐸 (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒)))
9692, 95anbi12d 624 . . . . . . . 8 (𝑔 = ((iEdg‘𝐵) ∘ ((iEdg‘𝐴))) → ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) ↔ (((iEdg‘𝐵) ∘ ((iEdg‘𝐴))):𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐴)))‘𝑒))))
9712, 91, 96elabd 3573 . . . . . . 7 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) → ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)))
9897ex 403 . . . . . 6 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → ((:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))) → ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))))
9998exlimdv 2032 . . . . 5 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))) → ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))))
1006cnvex 7380 . . . . . . . . . 10 (iEdg‘𝐵) ∈ V
101 vex 3417 . . . . . . . . . . 11 𝑔 ∈ V
102101, 8coex 7385 . . . . . . . . . 10 (𝑔 ∘ (iEdg‘𝐴)) ∈ V
103100, 102coex 7385 . . . . . . . . 9 ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V
104103a1i 11 . . . . . . . 8 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) ∈ V)
10515ad3antlr 722 . . . . . . . . . . 11 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto→ran (iEdg‘𝐵))
106 f1ocnv 6394 . . . . . . . . . . 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 6374 . . . . . . . . . . . . . 14 ((𝐸 = ran (iEdg‘𝐴) ∧ 𝐾 = ran (iEdg‘𝐵)) → (𝑔:𝐸1-1-onto𝐾𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵)))
10929, 18, 108mp2an 683 . . . . . . . . . . . . 13 (𝑔:𝐸1-1-onto𝐾𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
110109biimpi 208 . . . . . . . . . . . 12 (𝑔:𝐸1-1-onto𝐾𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
111110ad2antrl 719 . . . . . . . . . . 11 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → 𝑔:ran (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
11226ad3antrrr 721 . . . . . . . . . . 11 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐴))
113 f1oco 6404 . . . . . . . . . . 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 579 . . . . . . . . . 10 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)–1-1-onto→ran (iEdg‘𝐵))
115 f1oco 6404 . . . . . . . . . 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 579 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵))
11761ad2antrr 717 . . . . . . . . . . . . . 14 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐴))
118117ffund 6286 . . . . . . . . . . . . 13 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → Fun (iEdg‘𝐴))
119118adantr 474 . . . . . . . . . . . 12 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → Fun (iEdg‘𝐴))
120 fvelrn 6606 . . . . . . . . . . . 12 ((Fun (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
121119, 120sylan 575 . . . . . . . . . . 11 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴))
12229raleqi 3354 . . . . . . . . . . . . . . . 16 (∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒) ↔ ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
123122biimpi 208 . . . . . . . . . . . . . . 15 (∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
124123ad2antll 720 . . . . . . . . . . . . . 14 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
125124adantr 474 . . . . . . . . . . . . 13 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒))
126 imaeq2 5707 . . . . . . . . . . . . . . 15 (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑓𝑒) = (𝑓 “ ((iEdg‘𝐴)‘𝑖)))
127 fveq2 6437 . . . . . . . . . . . . . . 15 (𝑒 = ((iEdg‘𝐴)‘𝑖) → (𝑔𝑒) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
128126, 127eqeq12d 2840 . . . . . . . . . . . . . 14 (𝑒 = ((iEdg‘𝐴)‘𝑖) → ((𝑓𝑒) = (𝑔𝑒) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖))))
129128rspccva 3525 . . . . . . . . . . . . 13 ((∀𝑒 ∈ ran (iEdg‘𝐴)(𝑓𝑒) = (𝑔𝑒) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
130125, 129sylan 575 . . . . . . . . . . . 12 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
131 feq3 6265 . . . . . . . . . . . . . . . . . . . 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 226 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
134133ad2antrr 717 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
135 f1ofn 6383 . . . . . . . . . . . . . . . . . 18 (𝑔:𝐸1-1-onto𝐾𝑔 Fn 𝐸)
136135adantr 474 . . . . . . . . . . . . . . . . 17 ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → 𝑔 Fn 𝐸)
137134, 136anim12ci 607 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
138137ad2antrr 717 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔 Fn 𝐸 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
139 fnfco 6310 . . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → 𝑖 ∈ dom (iEdg‘𝐴))
142141adantr 474 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → 𝑖 ∈ dom (iEdg‘𝐴))
143 fvco2 6524 . . . . . . . . . . . . . 14 (((𝑔 ∘ (iEdg‘𝐴)) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
144140, 142, 143syl2anc 579 . . . . . . . . . . . . 13 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)))
145 f1of 6382 . . . . . . . . . . . . . . . . . . . . 21 ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto𝐾 → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
14621, 145syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝐵 ∈ USHGraph → (iEdg‘𝐵):dom (iEdg‘𝐵)⟶𝐾)
147146ffund 6286 . . . . . . . . . . . . . . . . . . 19 (𝐵 ∈ USHGraph → Fun (iEdg‘𝐵))
148 funcocnv2 6406 . . . . . . . . . . . . . . . . . . 19 (Fun (iEdg‘𝐵) → ((iEdg‘𝐵) ∘ (iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
149147, 148syl 17 . . . . . . . . . . . . . . . . . 18 (𝐵 ∈ USHGraph → ((iEdg‘𝐵) ∘ (iEdg‘𝐵)) = ( I ↾ ran (iEdg‘𝐵)))
150149eqcomd 2831 . . . . . . . . . . . . . . . . 17 (𝐵 ∈ USHGraph → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ (iEdg‘𝐵)))
151150ad5antlr 730 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ( I ↾ ran (iEdg‘𝐵)) = ((iEdg‘𝐵) ∘ (iEdg‘𝐵)))
152151coeq1d 5520 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = (((iEdg‘𝐵) ∘ (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))))
153152fveq1d 6439 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = ((((iEdg‘𝐵) ∘ (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
154 coass 5899 . . . . . . . . . . . . . . 15 (((iEdg‘𝐵) ∘ (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴))) = ((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))
155154fveq1i 6438 . . . . . . . . . . . . . 14 ((((iEdg‘𝐵) ∘ (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖)
156153, 155syl6eq 2877 . . . . . . . . . . . . 13 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((( I ↾ ran (iEdg‘𝐵)) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
157 f1of 6382 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:𝐸1-1-onto𝐾𝑔:𝐸𝐾)
158 eqid 2825 . . . . . . . . . . . . . . . . . . . . . 22 𝐸 = 𝐸
159158, 18feq23i 6276 . . . . . . . . . . . . . . . . . . . . 21 (𝑔:𝐸𝐾𝑔:𝐸⟶ran (iEdg‘𝐵))
160157, 159sylib 210 . . . . . . . . . . . . . . . . . . . 20 (𝑔:𝐸1-1-onto𝐾𝑔:𝐸⟶ran (iEdg‘𝐵))
161160adantr 474 . . . . . . . . . . . . . . . . . . 19 ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → 𝑔:𝐸⟶ran (iEdg‘𝐵))
162 f1of 6382 . . . . . . . . . . . . . . . . . . . . 21 ((iEdg‘𝐴):dom (iEdg‘𝐴)–1-1-onto𝐸 → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
16332, 162syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ USHGraph → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
164163ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
165 fco 6299 . . . . . . . . . . . . . . . . . . 19 ((𝑔:𝐸⟶ran (iEdg‘𝐵) ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
166161, 164, 165syl2anr 590 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵))
167166anim1i 608 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
168167adantr 474 . . . . . . . . . . . . . . . 16 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶ran (iEdg‘𝐵) ∧ 𝑖 ∈ dom (iEdg‘𝐴)))
169 ffvelrn 6611 . . . . . . . . . . . . . . . 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 6696 . . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸)
174173anim1i 608 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸𝑖 ∈ dom (iEdg‘𝐴)))
175174adantr 474 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸𝑖 ∈ dom (iEdg‘𝐴)))
176 fvco3 6526 . . . . . . . . . . . . . . 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 2861 . . . . . . . . . . . . 13 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (( I ↾ ran (iEdg‘𝐵))‘((𝑔 ∘ (iEdg‘𝐴))‘𝑖)) = (𝑔‘((iEdg‘𝐴)‘𝑖)))
179144, 156, 1783eqtr3rd 2870 . . . . . . . . . . . 12 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔‘((iEdg‘𝐴)‘𝑖)) = (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖))
180 dff1o4 6390 . . . . . . . . . . . . . . . . 17 ((iEdg‘𝐵):dom (iEdg‘𝐵)–1-1-onto𝐾 ↔ ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ (iEdg‘𝐵) Fn 𝐾))
18121, 180sylib 210 . . . . . . . . . . . . . . . 16 (𝐵 ∈ USHGraph → ((iEdg‘𝐵) Fn dom (iEdg‘𝐵) ∧ (iEdg‘𝐵) Fn 𝐾))
182181simprd 491 . . . . . . . . . . . . . . 15 (𝐵 ∈ USHGraph → (iEdg‘𝐵) Fn 𝐾)
183182ad5antlr 730 . . . . . . . . . . . . . 14 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (iEdg‘𝐵) Fn 𝐾)
184157adantr 474 . . . . . . . . . . . . . . . . 17 ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → 𝑔:𝐸𝐾)
185134, 184anim12ci 607 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → (𝑔:𝐸𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
186185ad2antrr 717 . . . . . . . . . . . . . . 15 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑔:𝐸𝐾 ∧ (iEdg‘𝐴):dom (iEdg‘𝐴)⟶𝐸))
187 fco 6299 . . . . . . . . . . . . . . 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 6310 . . . . . . . . . . . . . 14 (((iEdg‘𝐵) Fn 𝐾 ∧ (𝑔 ∘ (iEdg‘𝐴)):dom (iEdg‘𝐴)⟶𝐾) → ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
190183, 188, 189syl2anc 579 . . . . . . . . . . . . 13 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴))
191 fvco2 6524 . . . . . . . . . . . . 13 ((((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) Fn dom (iEdg‘𝐴) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
192190, 142, 191syl2anc 579 . . . . . . . . . . . 12 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (((iEdg‘𝐵) ∘ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))))‘𝑖) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
193130, 179, 1923eqtrd 2865 . . . . . . . . . . 11 ((((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) ∧ ((iEdg‘𝐴)‘𝑖) ∈ ran (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
194121, 193mpdan 678 . . . . . . . . . 10 (((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) ∧ 𝑖 ∈ dom (iEdg‘𝐴)) → (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
195194ralrimiva 3175 . . . . . . . . 9 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
196116, 195jca 507 . . . . . . . 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 6371 . . . . . . . . 9 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ↔ ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))):dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵)))
198 fveq1 6436 . . . . . . . . . . . 12 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (𝑖) = (((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))
199198fveq2d 6441 . . . . . . . . . . 11 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((iEdg‘𝐵)‘(𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖)))
200199eqeq2d 2835 . . . . . . . . . 10 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → ((𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) ↔ (𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
201200ralbidv 3195 . . . . . . . . 9 ( = ((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴))) → (∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(((iEdg‘𝐵) ∘ (𝑔 ∘ (iEdg‘𝐴)))‘𝑖))))
202197, 201anbi12d 624 . . . . . . . 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, 202elabd 3573 . . . . . . 7 ((((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) ∧ (𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))) → ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))))
204203ex 403 . . . . . 6 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → ((𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))))
205204exlimdv 2032 . . . . 5 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)) → ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))))
20699, 205impbid 204 . . . 4 (((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) ∧ 𝑓:𝑉1-1-onto𝑊) → (∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖))) ↔ ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒))))
207206pm5.32da 574 . . 3 ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → ((𝑓:𝑉1-1-onto𝑊 ∧ ∃(:dom (iEdg‘𝐴)–1-1-onto→dom (iEdg‘𝐵) ∧ ∀𝑖 ∈ dom (iEdg‘𝐴)(𝑓 “ ((iEdg‘𝐴)‘𝑖)) = ((iEdg‘𝐵)‘(𝑖)))) ↔ (𝑓:𝑉1-1-onto𝑊 ∧ ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)))))
208207exbidv 2020 . 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 271 1 ((𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph) → (𝐴 IsomGr 𝐵 ↔ ∃𝑓(𝑓:𝑉1-1-onto𝑊 ∧ ∃𝑔(𝑔:𝐸1-1-onto𝐾 ∧ ∀𝑒𝐸 (𝑓𝑒) = (𝑔𝑒)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1656  ∃wex 1878   ∈ wcel 2164  ∀wral 3117  ∃wrex 3118  Vcvv 3414   ∖ cdif 3795  ∅c0 4146  𝒫 cpw 4380  {csn 4399   class class class wbr 4875   I cid 5251  ◡ccnv 5345  dom cdm 5346  ran crn 5347   ↾ cres 5348   “ cima 5349   ∘ ccom 5350  Fun wfun 6121   Fn wfn 6122  ⟶wf 6123  –1-1→wf1 6124  –1-1-onto→wf1o 6126  ‘cfv 6127  Vtxcvtx 26301  iEdgciedg 26302  Edgcedg 26352  USHGraphcushgr 26362   IsomGr cisomgr 42555 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-op 4406  df-uni 4661  df-br 4876  df-opab 4938  df-mpt 4955  df-id 5252  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-edg 26353  df-ushgr 26364  df-isomgr 42557 This theorem is referenced by:  isomuspgr  42570
 Copyright terms: Public domain W3C validator