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 bilani ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝑀 : ( Edg ‘ 𝐺 ) –1-1-onto→ 𝐷 )
43 f1oeq3 ⊢ ( 𝐷 = ( Edg ‘ 𝐻 ) → ( 𝐽 : dom 𝐽 –1-1-onto→ 𝐷 ↔ 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ) )
44 4 43 ax-mp ⊢ ( 𝐽 : dom 𝐽 –1-1-onto→ 𝐷 ↔ 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
45 11 44 sylibr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐽 : dom 𝐽 –1-1-onto→ 𝐷 )
46 f1of ⊢ ( 𝐽 : dom 𝐽 –1-1-onto→ 𝐷 → 𝐽 : dom 𝐽 ⟶ 𝐷 )
47 45 46 syl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐽 : dom 𝐽 ⟶ 𝐷 )
48 47 ffvelcdmda ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( 𝐽 ‘ 𝑖 ) ∈ 𝐷 )
49 f1ocnvdm ⊢ ( ( 𝑀 : ( Edg ‘ 𝐺 ) –1-1-onto→ 𝐷 ∧ ( 𝐽 ‘ 𝑖 ) ∈ 𝐷 ) → ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) )
50 42 48 49 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) )
51 f1ocnvdm ⊢ ( ( 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) ∧ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) ) → ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ∈ dom 𝐼 )
52 39 50 51 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ∈ dom 𝐼 )
53 simpll1 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐺 ∈ USPGraph )
54 53 37 syl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) )
55 simpr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝑀 : 𝐸 –1-1-onto→ 𝐷 )
56 f1ocnvdm ⊢ ( ( 𝑀 : 𝐸 –1-1-onto→ 𝐷 ∧ ( 𝐽 ‘ 𝑖 ) ∈ 𝐷 ) → ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ 𝐸 )
57 55 48 56 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ 𝐸 )
58 57 3 eleqtrdi ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) )
59 f1ocnvfv2 ⊢ ( ( 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) ∧ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐺 ) ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ) = ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) )
60 54 58 59 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ) = ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) )
61 60 fveq2d ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( 𝑀 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ) ) = ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) )
62 f1ocnvfv2 ⊢ ( ( 𝑀 : 𝐸 –1-1-onto→ 𝐷 ∧ ( 𝐽 ‘ 𝑖 ) ∈ 𝐷 ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) = ( 𝐽 ‘ 𝑖 ) )
63 55 48 62 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( 𝑀 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) = ( 𝐽 ‘ 𝑖 ) )
64 61 63 eqtr2d ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ◡ 𝑀 ‘ ( 𝐽 ‘ 𝑖 ) ) ) ) ) )
65 36 52 64 rspcedvdw ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ∃ 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) )
66 eqtr2 ⊢ ( ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) )
67 f1of1 ⊢ ( 𝑀 : 𝐸 –1-1-onto→ 𝐷 → 𝑀 : 𝐸 –1-1→ 𝐷 )
68 67 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝑀 : 𝐸 –1-1→ 𝐷 )
69 68 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → 𝑀 : 𝐸 –1-1→ 𝐷 )
70 5 iedgedg ⊢ ( ( Fun 𝐼 ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑥 ) ∈ ( Edg ‘ 𝐺 ) )
71 17 70 sylan ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑥 ) ∈ ( Edg ‘ 𝐺 ) )
72 71 3 eleqtrrdi ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 )
73 72 ex ⊢ ( 𝐺 ∈ USPGraph → ( 𝑥 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ) )
74 5 iedgedg ⊢ ( ( Fun 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑦 ) ∈ ( Edg ‘ 𝐺 ) )
75 17 74 sylan ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑦 ) ∈ ( Edg ‘ 𝐺 ) )
76 75 3 eleqtrrdi ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑦 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 )
77 76 ex ⊢ ( 𝐺 ∈ USPGraph → ( 𝑦 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) )
78 73 77 anim12d ⊢ ( 𝐺 ∈ USPGraph → ( ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) ) )
79 78 3ad2ant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → ( ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) ) )
80 79 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) ) )
81 80 imp ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) )
82 f1fveq ⊢ ( ( 𝑀 : 𝐸 –1-1→ 𝐷 ∧ ( ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 ∧ ( 𝐼 ‘ 𝑦 ) ∈ 𝐸 ) ) → ( ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ↔ ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) ) )
83 69 81 82 syl2an2r ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ↔ ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) ) )
84 f1of1 ⊢ ( 𝐼 : dom 𝐼 –1-1-onto→ ( Edg ‘ 𝐺 ) → 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) )
85 37 84 syl ⊢ ( 𝐺 ∈ USPGraph → 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) )
86 85 3ad2ant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) )
87 86 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) )
88 f1veqaeq ⊢ ( ( 𝐼 : dom 𝐼 –1-1→ ( Edg ‘ 𝐺 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
89 87 88 sylan ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
90 83 89 sylbid ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) → 𝑥 = 𝑦 ) )
91 66 90 syl5 ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ) → ( ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) )
92 91 ralrimivva ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) )
93 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) )
94 93 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ↔ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ) )
95 94 reu4 ⊢ ( ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ↔ ( ∃ 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∧ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∧ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 ) ) )
96 65 92 95 sylanbrc ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) )
97 10 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
98 13 ad2antrr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → 𝑀 : 𝐸 ⟶ 𝐷 )
99 27 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → 𝐼 : dom 𝐼 ⟶ 𝐸 )
100 99 ffvelcdmda ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑥 ) ∈ 𝐸 )
101 98 100 ffvelcdmd ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∈ 𝐷 )
102 101 4 eleqtrdi ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐻 ) )
103 f1ocnvfv2 ⊢ ( ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) )
104 97 102 103 syl2an2r ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) )
105 104 eqeq2d ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ↔ ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) )
106 105 reubidva ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ↔ ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) )
107 96 106 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) )
108 11 ad2antrr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) )
109 f1of1 ⊢ ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) → 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) )
110 108 109 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) )
111 simplr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → 𝑖 ∈ dom 𝐽 )
112 33 adantlr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 )
113 f1fveq ⊢ ( ( 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) ∧ ( 𝑖 ∈ dom 𝐽 ∧ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 ) ) → ( ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ↔ 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) )
114 113 bicomd ⊢ ( ( 𝐽 : dom 𝐽 –1-1→ ( Edg ‘ 𝐻 ) ∧ ( 𝑖 ∈ dom 𝐽 ∧ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 ) ) → ( 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ↔ ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ) )
115 110 111 112 114 syl12anc ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) ∧ 𝑥 ∈ dom 𝐼 ) → ( 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ↔ ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ) )
116 115 reubidva ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ( ∃! 𝑥 ∈ dom 𝐼 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ↔ ∃! 𝑥 ∈ dom 𝐼 ( 𝐽 ‘ 𝑖 ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) ) )
117 107 116 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐽 ) → ∃! 𝑥 ∈ dom 𝐼 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) )
118 117 ralrimiva ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → ∀ 𝑖 ∈ dom 𝐽 ∃! 𝑥 ∈ dom 𝐼 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) )
119 8 f1ompt ⊢ ( 𝑁 : dom 𝐼 –1-1-onto→ dom 𝐽 ↔ ( ∀ 𝑥 ∈ dom 𝐼 ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ∈ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐽 ∃! 𝑥 ∈ dom 𝐼 𝑖 = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) ) )
120 34 118 119 sylanbrc ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → 𝑁 : dom 𝐼 –1-1-onto→ dom 𝐽 )
121 2fveq3 ⊢ ( 𝑥 = 𝑖 → ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) )
122 121 fveq2d ⊢ ( 𝑥 = 𝑖 → ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) )
123 122 adantl ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) ∧ 𝑥 = 𝑖 ) → ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑥 ) ) ) = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) )
124 simpr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → 𝑖 ∈ dom 𝐼 )
125 fvexd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) ∈ V )
126 8 123 124 125 fvmptd2 ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝑁 ‘ 𝑖 ) = ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) )
127 126 fveq2d ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐽 ‘ ( 𝑁 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) ) )
128 13 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → 𝑀 : 𝐸 ⟶ 𝐷 )
129 28 ffvelcdmda ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑖 ) ∈ 𝐸 )
130 128 129 ffvelcdmd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ∈ 𝐷 )
131 130 4 eleqtrdi ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐻 ) )
132 f1ocnvfv2 ⊢ ( ( 𝐽 : dom 𝐽 –1-1-onto→ ( Edg ‘ 𝐻 ) ∧ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ∈ ( Edg ‘ 𝐻 ) ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) )
133 11 131 132 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐽 ‘ ( ◡ 𝐽 ‘ ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) ) ) = ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) )
134 simpr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) ∧ 𝑥 = ( 𝐼 ‘ 𝑖 ) ) → 𝑥 = ( 𝐼 ‘ 𝑖 ) )
135 134 imaeq2d ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) ∧ 𝑥 = ( 𝐼 ‘ 𝑖 ) ) → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) )
136 simp3 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → 𝐹 ∈ 𝑋 )
137 136 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → 𝐹 ∈ 𝑋 )
138 137 imaexd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) ∈ V )
139 7 135 129 138 fvmptd2 ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝑀 ‘ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) )
140 127 133 139 3eqtrd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) ∧ 𝑖 ∈ dom 𝐼 ) → ( 𝐽 ‘ ( 𝑁 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) )
141 140 ralrimiva ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑁 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) )
142 120 141 jca ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑀 : 𝐸 –1-1-onto→ 𝐷 ) → ( 𝑁 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑁 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐼 ‘ 𝑖 ) ) ) )