Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isuspgrim0 Structured version   Visualization version   GIF version

Theorem isuspgrim0 47872
Description: An isomorphism of simple pseudographs is a bijection between their vertices which induces a bijection between their edges. (Contributed by AV, 21-Apr-2025.)
Hypotheses
Ref Expression
isusgrim.v 𝑉 = (Vtx‘𝐺)
isusgrim.w 𝑊 = (Vtx‘𝐻)
isusgrim.e 𝐸 = (Edg‘𝐺)
isusgrim.d 𝐷 = (Edg‘𝐻)
Assertion
Ref Expression
isuspgrim0 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)))
Distinct variable groups:   𝐷,𝑒   𝑒,𝐸   𝑒,𝐹   𝑒,𝐺   𝑒,𝐻   𝑒,𝑉   𝑒,𝑊   𝑒,𝑋

Proof of Theorem isuspgrim0
Dummy variables 𝑑 𝑖 𝑥 𝑗 𝑘 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isusgrim.v . . 3 𝑉 = (Vtx‘𝐺)
2 isusgrim.w . . 3 𝑊 = (Vtx‘𝐻)
3 eqid 2737 . . 3 (iEdg‘𝐺) = (iEdg‘𝐺)
4 eqid 2737 . . 3 (iEdg‘𝐻) = (iEdg‘𝐻)
51, 2, 3, 4isgrim 47868 . 2 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉1-1-onto𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))))))
6 isusgrim.e . . . . . . . . . . . . . . 15 𝐸 = (Edg‘𝐺)
76eleq2i 2833 . . . . . . . . . . . . . 14 (𝑒𝐸𝑒 ∈ (Edg‘𝐺))
8 uspgruhgr 29201 . . . . . . . . . . . . . . 15 (𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph)
93uhgredgiedgb 29143 . . . . . . . . . . . . . . 15 (𝐺 ∈ UHGraph → (𝑒 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘)))
108, 9syl 17 . . . . . . . . . . . . . 14 (𝐺 ∈ USPGraph → (𝑒 ∈ (Edg‘𝐺) ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘)))
117, 10bitrid 283 . . . . . . . . . . . . 13 (𝐺 ∈ USPGraph → (𝑒𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘)))
12113ad2ant1 1134 . . . . . . . . . . . 12 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) → (𝑒𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘)))
1312ad2antrr 726 . . . . . . . . . . 11 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝑒𝐸 ↔ ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘)))
1413biimpa 476 . . . . . . . . . 10 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒𝐸) → ∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘))
15 2fveq3 6911 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → ((iEdg‘𝐻)‘(𝑗𝑖)) = ((iEdg‘𝐻)‘(𝑗𝑘)))
16 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑖 = 𝑘 → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘𝑘))
1716imaeq2d 6078 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑘 → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
1815, 17eqeq12d 2753 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑘 → (((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
1918rspcv 3618 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
2019adantl 481 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((iEdg‘𝐻)‘(𝑗𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘))))
21 uspgruhgr 29201 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph)
224uhgrfun 29083 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐻 ∈ UHGraph → Fun (iEdg‘𝐻))
2321, 22syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐻 ∈ USPGraph → Fun (iEdg‘𝐻))
24233ad2ant2 1135 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) → Fun (iEdg‘𝐻))
2524ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → Fun (iEdg‘𝐻))
26 f1of 6848 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
2726adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → 𝑗:dom (iEdg‘𝐺)⟶dom (iEdg‘𝐻))
2827ffvelcdmda 7104 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝑗𝑘) ∈ dom (iEdg‘𝐻))
294iedgedg 29067 . . . . . . . . . . . . . . . . . . . . 21 ((Fun (iEdg‘𝐻) ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐻)) → ((iEdg‘𝐻)‘(𝑗𝑘)) ∈ (Edg‘𝐻))
3025, 28, 29syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑗𝑘)) ∈ (Edg‘𝐻))
31 isusgrim.d . . . . . . . . . . . . . . . . . . . . 21 𝐷 = (Edg‘𝐻)
3231eleq2i 2833 . . . . . . . . . . . . . . . . . . . 20 (((iEdg‘𝐻)‘(𝑗𝑘)) ∈ 𝐷 ↔ ((iEdg‘𝐻)‘(𝑗𝑘)) ∈ (Edg‘𝐻))
3330, 32sylibr 234 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐻)‘(𝑗𝑘)) ∈ 𝐷)
34 eleq1 2829 . . . . . . . . . . . . . . . . . . 19 (((iEdg‘𝐻)‘(𝑗𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (((iEdg‘𝐻)‘(𝑗𝑘)) ∈ 𝐷 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
3533, 34syl5ibcom 245 . . . . . . . . . . . . . . . . . 18 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (((iEdg‘𝐻)‘(𝑗𝑘)) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
3620, 35syld 47 . . . . . . . . . . . . . . . . 17 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
3736ex 412 . . . . . . . . . . . . . . . 16 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (𝑘 ∈ dom (iEdg‘𝐺) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)))
3837com23 86 . . . . . . . . . . . . . . 15 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → (𝑘 ∈ dom (iEdg‘𝐺) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)))
3938impr 454 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝑘 ∈ dom (iEdg‘𝐺) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
4039adantr 480 . . . . . . . . . . . . 13 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒𝐸) → (𝑘 ∈ dom (iEdg‘𝐺) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
4140imp 406 . . . . . . . . . . . 12 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒𝐸) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷)
42 imaeq2 6074 . . . . . . . . . . . . 13 (𝑒 = ((iEdg‘𝐺)‘𝑘) → (𝐹𝑒) = (𝐹 “ ((iEdg‘𝐺)‘𝑘)))
4342eleq1d 2826 . . . . . . . . . . . 12 (𝑒 = ((iEdg‘𝐺)‘𝑘) → ((𝐹𝑒) ∈ 𝐷 ↔ (𝐹 “ ((iEdg‘𝐺)‘𝑘)) ∈ 𝐷))
4441, 43syl5ibrcom 247 . . . . . . . . . . 11 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒𝐸) ∧ 𝑘 ∈ dom (iEdg‘𝐺)) → (𝑒 = ((iEdg‘𝐺)‘𝑘) → (𝐹𝑒) ∈ 𝐷))
4544rexlimdva 3155 . . . . . . . . . 10 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒𝐸) → (∃𝑘 ∈ dom (iEdg‘𝐺)𝑒 = ((iEdg‘𝐺)‘𝑘) → (𝐹𝑒) ∈ 𝐷))
4614, 45mpd 15 . . . . . . . . 9 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑒𝐸) → (𝐹𝑒) ∈ 𝐷)
4746ralrimiva 3146 . . . . . . . 8 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ∀𝑒𝐸 (𝐹𝑒) ∈ 𝐷)
4831eleq2i 2833 . . . . . . . . . . . . 13 (𝑑𝐷𝑑 ∈ (Edg‘𝐻))
494uhgredgiedgb 29143 . . . . . . . . . . . . . 14 (𝐻 ∈ UHGraph → (𝑑 ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘)))
5021, 49syl 17 . . . . . . . . . . . . 13 (𝐻 ∈ USPGraph → (𝑑 ∈ (Edg‘𝐻) ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘)))
5148, 50bitrid 283 . . . . . . . . . . . 12 (𝐻 ∈ USPGraph → (𝑑𝐷 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘)))
52513ad2ant2 1135 . . . . . . . . . . 11 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) → (𝑑𝐷 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘)))
5352ad2antrr 726 . . . . . . . . . 10 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝑑𝐷 ↔ ∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘)))
54 simprl 771 . . . . . . . . . . . . 13 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → 𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻))
55 f1ocnvdm 7305 . . . . . . . . . . . . 13 ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗𝑘) ∈ dom (iEdg‘𝐺))
5654, 55sylan 580 . . . . . . . . . . . 12 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗𝑘) ∈ dom (iEdg‘𝐺))
57 2fveq3 6911 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗𝑘) → ((iEdg‘𝐻)‘(𝑗𝑖)) = ((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))))
58 fveq2 6906 . . . . . . . . . . . . . . . . . . 19 (𝑖 = (𝑗𝑘) → ((iEdg‘𝐺)‘𝑖) = ((iEdg‘𝐺)‘(𝑗𝑘)))
5958imaeq2d 6078 . . . . . . . . . . . . . . . . . 18 (𝑖 = (𝑗𝑘) → (𝐹 “ ((iEdg‘𝐺)‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))))
6057, 59eqeq12d 2753 . . . . . . . . . . . . . . . . 17 (𝑖 = (𝑗𝑘) → (((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
6160rspccv 3619 . . . . . . . . . . . . . . . 16 (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
6261adantl 481 . . . . . . . . . . . . . . 15 ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
6362adantl 481 . . . . . . . . . . . . . 14 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
6463adantr 480 . . . . . . . . . . . . 13 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → ((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
65 f1ocnvfv2 7297 . . . . . . . . . . . . . . . 16 ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗‘(𝑗𝑘)) = 𝑘)
6654, 65sylan 580 . . . . . . . . . . . . . . 15 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑗‘(𝑗𝑘)) = 𝑘)
6766fveqeq2d 6914 . . . . . . . . . . . . . 14 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) ↔ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
68 eqeq2 2749 . . . . . . . . . . . . . . . . 17 (((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → (𝑑 = ((iEdg‘𝐻)‘𝑘) ↔ 𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
6968adantl 481 . . . . . . . . . . . . . . . 16 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) → (𝑑 = ((iEdg‘𝐻)‘𝑘) ↔ 𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))))
70 simpll1 1213 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → 𝐺 ∈ USPGraph)
716, 3uspgriedgedg 29193 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐺 ∈ USPGraph ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → ∃!𝑒𝐸 𝑒 = ((iEdg‘𝐺)‘(𝑗𝑘)))
7270, 56, 71syl2an2r 685 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃!𝑒𝐸 𝑒 = ((iEdg‘𝐺)‘(𝑗𝑘)))
73 eqcom 2744 . . . . . . . . . . . . . . . . . . . . . 22 (((iEdg‘𝐺)‘(𝑗𝑘)) = 𝑒𝑒 = ((iEdg‘𝐺)‘(𝑗𝑘)))
7473reubii 3389 . . . . . . . . . . . . . . . . . . . . 21 (∃!𝑒𝐸 ((iEdg‘𝐺)‘(𝑗𝑘)) = 𝑒 ↔ ∃!𝑒𝐸 𝑒 = ((iEdg‘𝐺)‘(𝑗𝑘)))
7572, 74sylibr 234 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃!𝑒𝐸 ((iEdg‘𝐺)‘(𝑗𝑘)) = 𝑒)
76 f1of1 6847 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:𝑉1-1-onto𝑊𝐹:𝑉1-1𝑊)
7776ad4antlr 733 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒𝐸) → 𝐹:𝑉1-1𝑊)
78 uspgrupgr 29195 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)
79783ad2ant1 1134 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) → 𝐺 ∈ UPGraph)
8079ad3antrrr 730 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → 𝐺 ∈ UPGraph)
8180, 56jca 511 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝐺 ∈ UPGraph ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)))
8281adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒𝐸) → (𝐺 ∈ UPGraph ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)))
831, 3upgrss 29105 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐺 ∈ UPGraph ∧ (𝑗𝑘) ∈ dom (iEdg‘𝐺)) → ((iEdg‘𝐺)‘(𝑗𝑘)) ⊆ 𝑉)
8482, 83syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒𝐸) → ((iEdg‘𝐺)‘(𝑗𝑘)) ⊆ 𝑉)
857biimpi 216 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑒𝐸𝑒 ∈ (Edg‘𝐺))
86 edgupgr 29151 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐺 ∈ UPGraph ∧ 𝑒 ∈ (Edg‘𝐺)) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝑒 ≠ ∅ ∧ (♯‘𝑒) ≤ 2))
8780, 85, 86syl2an 596 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒𝐸) → (𝑒 ∈ 𝒫 (Vtx‘𝐺) ∧ 𝑒 ≠ ∅ ∧ (♯‘𝑒) ≤ 2))
8887simp1d 1143 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒𝐸) → 𝑒 ∈ 𝒫 (Vtx‘𝐺))
8988elpwid 4609 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒𝐸) → 𝑒 ⊆ (Vtx‘𝐺))
9089, 1sseqtrrdi 4025 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒𝐸) → 𝑒𝑉)
91 f1imaeq 7285 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹:𝑉1-1𝑊 ∧ (((iEdg‘𝐺)‘(𝑗𝑘)) ⊆ 𝑉𝑒𝑉)) → ((𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) = (𝐹𝑒) ↔ ((iEdg‘𝐺)‘(𝑗𝑘)) = 𝑒))
9277, 84, 90, 91syl12anc 837 . . . . . . . . . . . . . . . . . . . . 21 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ 𝑒𝐸) → ((𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) = (𝐹𝑒) ↔ ((iEdg‘𝐺)‘(𝑗𝑘)) = 𝑒))
9392reubidva 3396 . . . . . . . . . . . . . . . . . . . 20 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (∃!𝑒𝐸 (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) = (𝐹𝑒) ↔ ∃!𝑒𝐸 ((iEdg‘𝐺)‘(𝑗𝑘)) = 𝑒))
9475, 93mpbird 257 . . . . . . . . . . . . . . . . . . 19 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ∃!𝑒𝐸 (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) = (𝐹𝑒))
9594ad2antrr 726 . . . . . . . . . . . . . . . . . 18 (((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) ∧ 𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) → ∃!𝑒𝐸 (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) = (𝐹𝑒))
96 eqeq1 2741 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → (𝑑 = (𝐹𝑒) ↔ (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) = (𝐹𝑒)))
9796reubidv 3398 . . . . . . . . . . . . . . . . . . 19 (𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → (∃!𝑒𝐸 𝑑 = (𝐹𝑒) ↔ ∃!𝑒𝐸 (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) = (𝐹𝑒)))
9897adantl 481 . . . . . . . . . . . . . . . . . 18 (((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) ∧ 𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) → (∃!𝑒𝐸 𝑑 = (𝐹𝑒) ↔ ∃!𝑒𝐸 (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) = (𝐹𝑒)))
9995, 98mpbird 257 . . . . . . . . . . . . . . . . 17 (((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) ∧ 𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) → ∃!𝑒𝐸 𝑑 = (𝐹𝑒))
10099ex 412 . . . . . . . . . . . . . . . 16 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) → (𝑑 = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → ∃!𝑒𝐸 𝑑 = (𝐹𝑒)))
10169, 100sylbid 240 . . . . . . . . . . . . . . 15 ((((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) ∧ ((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘)))) → (𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒𝐸 𝑑 = (𝐹𝑒)))
102101ex 412 . . . . . . . . . . . . . 14 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (((iEdg‘𝐻)‘𝑘) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → (𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒𝐸 𝑑 = (𝐹𝑒))))
10367, 102sylbid 240 . . . . . . . . . . . . 13 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (((iEdg‘𝐻)‘(𝑗‘(𝑗𝑘))) = (𝐹 “ ((iEdg‘𝐺)‘(𝑗𝑘))) → (𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒𝐸 𝑑 = (𝐹𝑒))))
10464, 103syld 47 . . . . . . . . . . . 12 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → ((𝑗𝑘) ∈ dom (iEdg‘𝐺) → (𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒𝐸 𝑑 = (𝐹𝑒))))
10556, 104mpd 15 . . . . . . . . . . 11 (((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ∧ 𝑘 ∈ dom (iEdg‘𝐻)) → (𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒𝐸 𝑑 = (𝐹𝑒)))
106105rexlimdva 3155 . . . . . . . . . 10 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (∃𝑘 ∈ dom (iEdg‘𝐻)𝑑 = ((iEdg‘𝐻)‘𝑘) → ∃!𝑒𝐸 𝑑 = (𝐹𝑒)))
10753, 106sylbid 240 . . . . . . . . 9 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝑑𝐷 → ∃!𝑒𝐸 𝑑 = (𝐹𝑒)))
108107ralrimiv 3145 . . . . . . . 8 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → ∀𝑑𝐷 ∃!𝑒𝐸 𝑑 = (𝐹𝑒))
109 imaeq2 6074 . . . . . . . . . 10 (𝑥 = 𝑒 → (𝐹𝑥) = (𝐹𝑒))
110109cbvmptv 5255 . . . . . . . . 9 (𝑥𝐸 ↦ (𝐹𝑥)) = (𝑒𝐸 ↦ (𝐹𝑒))
111110f1ompt 7131 . . . . . . . 8 ((𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷 ↔ (∀𝑒𝐸 (𝐹𝑒) ∈ 𝐷 ∧ ∀𝑑𝐷 ∃!𝑒𝐸 𝑑 = (𝐹𝑒)))
11247, 108, 111sylanbrc 583 . . . . . . 7 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) → (𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷)
113112ex 412 . . . . . 6 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷))
114113exlimdv 1933 . . . . 5 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) → (𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷))
115 fvex 6919 . . . . . . . . . 10 (iEdg‘𝐺) ∈ V
116115dmex 7931 . . . . . . . . 9 dom (iEdg‘𝐺) ∈ V
117116mptex 7243 . . . . . . . 8 (𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))) ∈ V
118117a1i 11 . . . . . . 7 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷) → (𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))) ∈ V)
119 eqid 2737 . . . . . . . 8 (𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))) = (𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒))))
1201, 2, 6, 31, 3, 4, 110, 119isuspgrim0lem 47871 . . . . . . 7 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷) → ((𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))):dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘((𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒))))‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))))
121 f1oeq1 6836 . . . . . . . 8 (𝑗 = (𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))) → (𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ↔ (𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))):dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻)))
122 fveq1 6905 . . . . . . . . . 10 (𝑗 = (𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))) → (𝑗𝑖) = ((𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒))))‘𝑖))
123122fveqeq2d 6914 . . . . . . . . 9 (𝑗 = (𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))) → (((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ((iEdg‘𝐻)‘((𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒))))‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))))
124123ralbidv 3178 . . . . . . . 8 (𝑗 = (𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))) → (∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)) ↔ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘((𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒))))‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))))
125121, 124anbi12d 632 . . . . . . 7 (𝑗 = (𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))) → ((𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ↔ ((𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒)))):dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘((𝑒 ∈ dom (iEdg‘𝐺) ↦ ((iEdg‘𝐻)‘((𝑥𝐸 ↦ (𝐹𝑥))‘((iEdg‘𝐺)‘𝑒))))‘𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
126118, 120, 125spcedv 3598 . . . . . 6 ((((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) ∧ (𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷) → ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))))
127126ex 412 . . . . 5 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) → ((𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷 → ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))))
128114, 127impbid 212 . . . 4 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ↔ (𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷))
129 f1oeq1 6836 . . . . 5 ((𝑥𝐸 ↦ (𝐹𝑥)) = (𝑒𝐸 ↦ (𝐹𝑒)) → ((𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷 ↔ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷))
130110, 129mp1i 13 . . . 4 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) → ((𝑥𝐸 ↦ (𝐹𝑥)):𝐸1-1-onto𝐷 ↔ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷))
131128, 130bitrd 279 . . 3 (((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) ∧ 𝐹:𝑉1-1-onto𝑊) → (∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖))) ↔ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷))
132131pm5.32da 579 . 2 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) → ((𝐹:𝑉1-1-onto𝑊 ∧ ∃𝑗(𝑗:dom (iEdg‘𝐺)–1-1-onto→dom (iEdg‘𝐻) ∧ ∀𝑖 ∈ dom (iEdg‘𝐺)((iEdg‘𝐻)‘(𝑗𝑖)) = (𝐹 “ ((iEdg‘𝐺)‘𝑖)))) ↔ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)))
1335, 132bitrd 279 1 ((𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹𝑋) → (𝐹 ∈ (𝐺 GraphIso 𝐻) ↔ (𝐹:𝑉1-1-onto𝑊 ∧ (𝑒𝐸 ↦ (𝐹𝑒)):𝐸1-1-onto𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wex 1779  wcel 2108  wne 2940  wral 3061  wrex 3070  ∃!wreu 3378  Vcvv 3480  wss 3951  c0 4333  𝒫 cpw 4600   class class class wbr 5143  cmpt 5225  ccnv 5684  dom cdm 5685  cima 5688  Fun wfun 6555  wf 6557  1-1wf1 6558  1-1-ontowf1o 6560  cfv 6561  (class class class)co 7431  cle 11296  2c2 12321  chash 14369  Vtxcvtx 29013  iEdgciedg 29014  Edgcedg 29064  UHGraphcuhgr 29073  UPGraphcupgr 29097  USPGraphcuspgr 29165   GraphIso cgrim 47861
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-oprab 7435  df-mpo 7436  df-map 8868  df-edg 29065  df-uhgr 29075  df-upgr 29099  df-uspgr 29167  df-grim 47864
This theorem is referenced by:  uspgrimprop  47873  isuspgrim  47875
  Copyright terms: Public domain W3C validator