Metamath Proof Explorer

Theorem isuspgrim0lem

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)

Ref Expression
Hypotheses isusgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isusgrim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
isusgrim.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
isusgrim.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
isuspgrim0lem.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
isuspgrim0lem.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
isuspgrim0lem.m ⊢ 𝑀 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) )
isuspgrim0lem.n ⊢ 𝑁 = ( 𝑥 ∈ dom 𝐼 ↦ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) )
Assertion isuspgrim0lem ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → ( 𝑁 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑁 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) ) )

Proof

Step Hyp Ref Expression
1 isusgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isusgrim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 isusgrim.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
4 isusgrim.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
5 isuspgrim0lem.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
6 isuspgrim0lem.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
7 isuspgrim0lem.m ⊢ 𝑀 = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) )
8 isuspgrim0lem.n ⊢ 𝑁 = ( 𝑥 ∈ dom 𝐼 ↦ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) )
9 6 uspgrf1oedg ⊢ ( 𝐻 ∈ USPGraph → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
10 9 3ad2ant2 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
11 10 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
12 f1of ⊢ ( 𝑀 : 𝐸 –1-1-onto→ 𝐷 → 𝑀 : 𝐸 ⟶ 𝐷 )
13 12 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝑀 : 𝐸 ⟶ 𝐷 )
14 13 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑥 ∈ dom 𝐼 ) → 𝑀 : 𝐸 ⟶ 𝐷 )
15 uspgruhgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
16 5 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐼 )
17 15 16 syl ⊢ ( 𝐺 ∈ USPGraph → Fun 𝐼 )
18 edgval ⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
19 5 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐼
20 19 rneqi ⊢ ran ( iEdg ‘ 𝐺 ) = ran 𝐼
21 3 18 20 3eqtri ⊢ 𝐸 = ran 𝐼
22 feq3 ⊢ ( 𝐸 = ran 𝐼 → ( 𝐼 : dom 𝐼 ⟶ 𝐸 ↔ 𝐼 : dom 𝐼 ⟶ ran 𝐼 ) )
23 21 22 ax-mp ⊢ ( 𝐼 : dom 𝐼 ⟶ 𝐸 ↔ 𝐼 : dom 𝐼 ⟶ ran 𝐼 )
24 fdmrn ⊢ ( Fun 𝐼 ↔ 𝐼 : dom 𝐼 ⟶ ran 𝐼 )
25 23 24 bitr4i ⊢ ( 𝐼 : dom 𝐼 ⟶ 𝐸 ↔ Fun 𝐼 )
26 17 25 sylibr ⊢ ( 𝐺 ∈ USPGraph → 𝐼 : dom 𝐼 ⟶ 𝐸 )
27 26 3ad2ant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → 𝐼 : dom 𝐼 ⟶ 𝐸 )
28 27 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐼 : dom 𝐼 ⟶ 𝐸 )
29 28 ffvelcdmda ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 )
30 14 29 ffvelcdmd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∈ 𝐷 )
31 30 4 eleqtrdi ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐻 ) )
32 f1ocnvdm ⊢ ( ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 )
33 11 31 32 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 )
34 33 ralrimiva ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → ∀ 𝑥 ∈ dom 𝐼 ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 )
35 2fveq3 ⊢ ( 𝑥 = ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ) ) )
36 35 eqeq2d ⊢ ( 𝑥 = ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) → ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ↔ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ) ) ) )
37 5 uspgrf1oedg ⊢ ( 𝐺 ∈ USPGraph → 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) )
38 37 3ad2ant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) )
39 38 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) )
40 f1oeq2 ⊢ ( 𝐸 = ( Edg ‘ 𝐺 ) → ( 𝑀 : 𝐸 –1-1-onto→ 𝐷 ↔ 𝑀 : ( Edg ‘ 𝐺 ) –1-1-onto→ 𝐷 ) )
41 3 40 ax-mp ⊢ ( 𝑀 : 𝐸 –1-1-onto→ 𝐷 ↔ 𝑀 : ( Edg ‘ 𝐺 ) –1-1-onto→ 𝐷 )
42 41 biimpi ⊢ ( 𝑀 : 𝐸 –1-1-onto→ 𝐷 → 𝑀 : ( Edg ‘ 𝐺 ) –1-1-onto→ 𝐷 )
43 42 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝑀 : ( Edg ‘ 𝐺 ) –1-1-onto→ 𝐷 )
44 f1oeq3 ⊢ ( 𝐷 = ( Edg ‘ 𝐻 ) → ( 𝐽 : dom 𝐽 –1-1-onto→ 𝐷 ↔ 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ) )
45 4 44 ax-mp ⊢ ( 𝐽 : dom 𝐽 –1-1-onto→ 𝐷 ↔ 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
46 11 45 sylibr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐽 : dom 𝐽 –1-1-onto→ 𝐷 )
47 f1of ⊢ ( 𝐽 : dom 𝐽 –1-1-onto→ 𝐷 → 𝐽 : dom 𝐽 ⟶ 𝐷 )
48 46 47 syl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐽 : dom 𝐽 ⟶ 𝐷 )
49 48 ffvelcdmda ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( 𝐽 ‘ 𝑖 ) ∈ 𝐷 )
50 f1ocnvdm ⊢ ( ( 𝑀 : ( Edg ‘ 𝐺 ) –1-1-onto→ 𝐷 ∧ ( 𝐽 ‘ 𝑖 ) ∈ 𝐷 ) → ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) )
51 43 49 50 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) )
52 f1ocnvdm ⊢ ( ( 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) ∧ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) ) → ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ∈ dom 𝐼 )
53 39 51 52 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ∈ dom 𝐼 )
54 simpll1 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐺 ∈ USPGraph )
55 54 37 syl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) )
56 simpr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝑀 : 𝐸 –1-1-onto→ 𝐷 )
57 f1ocnvdm ⊢ ( ( 𝑀 : 𝐸 –1-1-onto→ 𝐷 ∧ ( 𝐽 ‘ 𝑖 ) ∈ 𝐷 ) → ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ 𝐸 )
58 56 49 57 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ 𝐸 )
59 58 3 eleqtrdi ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) )
60 f1ocnvfv2 ⊢ ( ( 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) ∧ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ) = ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) )
61 55 59 60 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ) = ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) )
62 61 fveq2d ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( 𝑀 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ) ) = ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) )
63 f1ocnvfv2 ⊢ ( ( 𝑀 : 𝐸 –1-1-onto→ 𝐷 ∧ ( 𝐽 ‘ 𝑖 ) ∈ 𝐷 ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) = ( 𝐽 ‘ 𝑖 ) )
64 56 49 63 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) = ( 𝐽 ‘ 𝑖 ) )
65 62 64 eqtr2d ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ) ) )
66 36 53 65 rspcedvdw ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ∃ 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) )
67 eqtr2 ⊢ ( ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) )
68 f1of1 ⊢ ( 𝑀 : 𝐸 –1-1-onto→ 𝐷 → 𝑀 : 𝐸 –1-1→ 𝐷 )
69 68 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝑀 : 𝐸 –1-1→ 𝐷 )
70 69 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → 𝑀 : 𝐸 –1-1→ 𝐷 )
71 5 iedgedg ⊢ ( ( Fun 𝐼 ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑥 ) ∈ ( Edg ‘ 𝐺 ) )
72 17 71 sylan ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑥 ) ∈ ( Edg ‘ 𝐺 ) )
73 72 3 eleqtrrdi ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 )
74 73 ex ⊢ ( 𝐺 ∈ USPGraph → ( 𝑥 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ) )
75 5 iedgedg ⊢ ( ( Fun 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑦 ) ∈ ( Edg ‘ 𝐺 ) )
76 17 75 sylan ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑦 ) ∈ ( Edg ‘ 𝐺 ) )
77 76 3 eleqtrrdi ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 )
78 77 ex ⊢ ( 𝐺 ∈ USPGraph → ( 𝑦 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) )
79 74 78 anim12d ⊢ ( 𝐺 ∈ USPGraph → ( ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) ) )
80 79 3ad2ant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → ( ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) ) )
81 80 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) ) )
82 81 imp ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) )
83 f1fveq ⊢ ( ( 𝑀 : 𝐸 –1-1→ 𝐷 ∧ ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) ) → ( ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ↔ ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) ) )
84 70 82 83 syl2an2r ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ↔ ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) ) )
85 f1of1 ⊢ ( 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) → 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) )
86 37 85 syl ⊢ ( 𝐺 ∈ USPGraph → 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) )
87 86 3ad2ant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) )
88 87 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) )
89 f1veqaeq ⊢ ( ( 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
90 88 89 sylan ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
91 84 90 sylbid ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
92 67 91 syl5 ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) )
93 92 ralrimivva ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) )
94 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) )
95 94 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ↔ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ) )
96 95 reu4 ⊢ ( ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ↔ ( ∃ 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) ) )
97 66 93 96 sylanbrc ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) )
98 10 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
99 13 ad2antrr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → 𝑀 : 𝐸 ⟶ 𝐷 )
100 27 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → 𝐼 : dom 𝐼 ⟶ 𝐸 )
101 100 ffvelcdmda ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 )
102 99 101 ffvelcdmd ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∈ 𝐷 )
103 102 4 eleqtrdi ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐻 ) )
104 f1ocnvfv2 ⊢ ( ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) )
105 98 103 104 syl2an2r ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) )
106 105 eqeq2d ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ↔ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) )
107 106 reubidva ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ↔ ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) )
108 97 107 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) )
109 11 ad2antrr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
110 f1of1 ⊢ ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) → 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) )
111 109 110 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) )
112 simplr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → 𝑖 ∈ dom 𝐽 )
113 33 adantlr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 )
114 f1fveq ⊢ ( ( 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) ∧ ( 𝑖 ∈ dom 𝐽 ∧ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 ) ) → ( ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ↔ 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) )
115 114 bicomd ⊢ ( ( 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) ∧ ( 𝑖 ∈ dom 𝐽 ∧ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 ) ) → ( 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ↔ ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ) )
116 111 112 113 115 syl12anc ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ↔ ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ) )
117 116 reubidva ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ∃! 𝑥 ∈ dom 𝐼 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ↔ ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ) )
118 108 117 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ∃! 𝑥 ∈ dom 𝐼 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) )
119 118 ralrimiva ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → ∀ 𝑖 ∈ dom 𝐽 ∃! 𝑥 ∈ dom 𝐼 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) )
120 8 f1ompt ⊢ ( 𝑁 : dom 𝐼 –1-1-onto→ dom 𝐽 ↔ ( ∀ 𝑥 ∈ dom 𝐼 ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐽 ∃! 𝑥 ∈ dom 𝐼 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) )
121 34 119 120 sylanbrc ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝑁 : dom 𝐼 –1-1-onto→ dom 𝐽 )
122 2fveq3 ⊢ ( 𝑥 = 𝑖 → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) )
123 122 fveq2d ⊢ ( 𝑥 = 𝑖 → ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) )
124 123 adantl ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) ∧ 𝑥 = 𝑖 ) → ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) )
125 simpr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → 𝑖 ∈ dom 𝐼 )
126 fvexd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) ∈ V )
127 8 124 125 126 fvmptd2 ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝑁 ‘ 𝑖 ) = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) )
128 127 fveq2d ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐽 ‘ ( 𝑁 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) ) )
129 13 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → 𝑀 : 𝐸 ⟶ 𝐷 )
130 28 ffvelcdmda ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑖 ) ∈ 𝐸 )
131 129 130 ffvelcdmd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ∈ 𝐷 )
132 131 4 eleqtrdi ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐻 ) )
133 f1ocnvfv2 ⊢ ( ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) )
134 11 132 133 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) )
135 simpr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) ∧ 𝑥 = ( 𝐼 ‘ 𝑖 ) ) → 𝑥 = ( 𝐼 ‘ 𝑖 ) )
136 135 imaeq2d ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) ∧ 𝑥 = ( 𝐼 ‘ 𝑖 ) ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) )
137 simp3 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → 𝐹 ∈ 𝑋 )
138 137 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → 𝐹 ∈ 𝑋 )
139 138 imaexd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) ∈ V )
140 7 136 130 139 fvmptd2 ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) )
141 128 134 140 3eqtrd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐽 ‘ ( 𝑁 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) )
142 141 ralrimiva ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑁 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) )
143 121 142 jca ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → ( 𝑁 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑁 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) ) )