Metamath Proof Explorer

Theorem isuspgrim0

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 ‘ 𝐻 )
Assertion isuspgrim0 ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 isusgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isusgrim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 isusgrim.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
4 isusgrim.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
5 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
7 1 2 5 6 isgrim ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ) )
8 3 eleq2i ⊢ ( 𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ( Edg ‘ 𝐺 ) )
9 uspgruhgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
10 5 uhgredgiedgb ⊢ ( 𝐺 ∈ UHGraph → ( 𝑒 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
11 9 10 syl ⊢ ( 𝐺 ∈ USPGraph → ( 𝑒 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
12 8 11 bitrid ⊢ ( 𝐺 ∈ USPGraph → ( 𝑒 ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
13 12 3ad2ant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → ( 𝑒 ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
14 13 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( 𝑒 ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
15 14 biimpa ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑒 ∈ 𝐸 ) → ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) )
16 2fveq3 ⊢ ( 𝑖 = 𝑘 → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) )
17 fveq2 ⊢ ( 𝑖 = 𝑘 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) )
18 17 imaeq2d ⊢ ( 𝑖 = 𝑘 → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑖 = 𝑘 → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
20 19 rspcv ⊢ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
21 20 adantl ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
22 uspgruhgr ⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph )
23 6 uhgrfun ⊢ ( 𝐻 ∈ UHGraph → Fun ( iEdg ‘ 𝐻 ) )
24 22 23 syl ⊢ ( 𝐻 ∈ USPGraph → Fun ( iEdg ‘ 𝐻 ) )
25 24 3ad2ant2 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → Fun ( iEdg ‘ 𝐻 ) )
26 25 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → Fun ( iEdg ‘ 𝐻 ) )
27 f1of ⊢ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
28 27 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
29 28 ffvelcdmda ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐻 ) )
30 6 iedgedg ⊢ ( ( Fun ( iEdg ‘ 𝐻 ) ∧ ( 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ ( Edg ‘ 𝐻 ) )
31 26 29 30 syl2anc ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ ( Edg ‘ 𝐻 ) )
32 4 eleq2i ⊢ ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ 𝐷 ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ ( Edg ‘ 𝐻 ) )
33 31 32 sylibr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ 𝐷 )
34 eleq1 ⊢ ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ 𝐷 ↔ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
35 33 34 syl5ibcom ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
36 21 35 syld ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
37 36 ex ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) ) )
38 37 com23 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) ) )
39 38 impr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
40 39 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
41 40 imp ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 )
42 imaeq2 ⊢ ( 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( 𝐹 “ 𝑒 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
43 42 eleq1d ⊢ ( 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( ( 𝐹 “ 𝑒 ) ∈ 𝐷 ↔ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
44 41 43 syl5ibrcom ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) )
45 44 rexlimdva ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑒 ∈ 𝐸 ) → ( ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) )
46 15 45 mpd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝐹 “ 𝑒 ) ∈ 𝐷 )
47 46 ralrimiva ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) ∈ 𝐷 )
48 4 eleq2i ⊢ ( 𝑑 ∈ 𝐷 ↔ 𝑑 ∈ ( Edg ‘ 𝐻 ) )
49 6 uhgredgiedgb ⊢ ( 𝐻 ∈ UHGraph → ( 𝑑 ∈ ( Edg ‘ 𝐻 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
50 22 49 syl ⊢ ( 𝐻 ∈ USPGraph → ( 𝑑 ∈ ( Edg ‘ 𝐻 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
51 48 50 bitrid ⊢ ( 𝐻 ∈ USPGraph → ( 𝑑 ∈ 𝐷 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
52 51 3ad2ant2 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → ( 𝑑 ∈ 𝐷 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
53 52 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( 𝑑 ∈ 𝐷 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
54 simprl ⊢ ( ( ( ( 𝐺 ∈ 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 ⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) )
56 54 55 sylan ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) )
57 2fveq3 ⊢ ( 𝑖 = ( ◡ 𝑗 ‘ 𝑘 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
58 fveq2 ⊢ ( 𝑖 = ( ◡ 𝑗 ‘ 𝑘 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) )
59 58 imaeq2d ⊢ ( 𝑖 = ( ◡ 𝑗 ‘ 𝑘 ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
60 57 59 eqeq12d ⊢ ( 𝑖 = ( ◡ 𝑗 ‘ 𝑘 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
61 60 rspccv ⊢ ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
62 61 adantl ⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
63 62 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
64 63 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
65 f1ocnvfv2 ⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) = 𝑘 )
66 54 65 sylan ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) = 𝑘 )
67 66 fveqeq2d ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
68 eqeq2 ⊢ ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → ( 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ↔ 𝑑 = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
69 68 adantl ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) → ( 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ↔ 𝑑 = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
70 simpll1 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → 𝐺 ∈ USPGraph )
71 3 5 uspgriedgedg ⊢ ( ( 𝐺 ∈ USPGraph ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ∃! 𝑒 ∈ 𝐸 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) )
72 70 56 71 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ∃! 𝑒 ∈ 𝐸 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) )
73 eqcom ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) = 𝑒 ↔ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) )
74 73 reubii ⊢ ( ∃! 𝑒 ∈ 𝐸 ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) = 𝑒 ↔ ∃! 𝑒 ∈ 𝐸 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) )
75 72 74 sylibr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ∃! 𝑒 ∈ 𝐸 ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) = 𝑒 )
76 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 –1-1→ 𝑊 )
77 76 ad4antlr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑒 ∈ 𝐸 ) → 𝐹 : 𝑉 –1-1→ 𝑊 )
78 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
79 78 3ad2ant1 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → 𝐺 ∈ UPGraph )
80 79 ad3antrrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → 𝐺 ∈ UPGraph )
81 80 56 jca ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( 𝐺 ∈ UPGraph ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
82 81 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝐺 ∈ UPGraph ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
83 1 5 upgrss ⊢ ( ( 𝐺 ∈ UPGraph ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ⊆ 𝑉 )
84 82 83 syl ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑒 ∈ 𝐸 ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ⊆ 𝑉 )
85 8 biimpi ⊢ ( 𝑒 ∈ 𝐸 → 𝑒 ∈ ( Edg ‘ 𝐺 ) )
86 edgupgr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝑒 ≠ ∅ ∧ ( ♯ ‘ 𝑒 ) ≤ 2 ) )
87 80 85 86 syl2an ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝑒 ≠ ∅ ∧ ( ♯ ‘ 𝑒 ) ≤ 2 ) )
88 87 simp1d ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
89 88 elpwid ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ⊆ ( Vtx ‘ 𝐺 ) )
90 89 1 sseqtrrdi ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ⊆ 𝑉 )
91 f1imaeq ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ⊆ 𝑉 ∧ 𝑒 ⊆ 𝑉 ) ) → ( ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ 𝑒 ) ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) = 𝑒 ) )
92 77 84 90 91 syl12anc ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑒 ∈ 𝐸 ) → ( ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ 𝑒 ) ↔ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) = 𝑒 ) )
93 92 reubidva ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ 𝑒 ) ↔ ∃! 𝑒 ∈ 𝐸 ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) = 𝑒 ) )
94 75 93 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ 𝑒 ) )
95 94 ad2antrr ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) ∧ 𝑑 = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) → ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ 𝑒 ) )
96 eqeq1 ⊢ ( 𝑑 = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → ( 𝑑 = ( 𝐹 “ 𝑒 ) ↔ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ 𝑒 ) ) )
97 96 reubidv ⊢ ( 𝑑 = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → ( ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ↔ ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ 𝑒 ) ) )
98 97 adantl ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) ∧ 𝑑 = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) → ( ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ↔ ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ 𝑒 ) ) )
99 95 98 mpbird ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) ∧ 𝑑 = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) )
100 99 ex ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) → ( 𝑑 = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) )
101 69 100 sylbid ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) → ( 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) )
102 101 ex ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → ( 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) )
103 67 102 sylbid ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → ( 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) )
104 64 103 syld ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) )
105 56 104 mpd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) )
106 105 rexlimdva ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝑑 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) )
107 53 106 sylbid ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) )
108 107 ralrimiv ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ∀ 𝑑 ∈ 𝐷 ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) )
109 imaeq2 ⊢ ( 𝑥 = 𝑒 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑒 ) )
110 109 cbvmptv ⊢ ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) = ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) )
111 110 f1ompt ⊢ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐷 ↔ ( ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) ∈ 𝐷 ∧ ∀ 𝑑 ∈ 𝐷 ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) )
112 47 108 111 sylanbrc ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐷 )
113 112 ex ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐷 ) )
114 113 exlimdv ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐷 ) )
115 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
116 115 dmex ⊢ dom ( iEdg ‘ 𝐺 ) ∈ V
117 116 mptex ⊢ ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) ∈ V
118 117 a1i ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) ∈ V )
119 eqid ⊢ ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) = ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) )
120 1 2 3 4 5 6 110 119 isuspgrim0lem ⊢ ( ( ( ( 𝐺 ∈ 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 ⊢ ( 𝑗 = ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) → ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ↔ ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) )
122 fveq1 ⊢ ( 𝑗 = ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) → ( 𝑗 ‘ 𝑖 ) = ( ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) ‘ 𝑖 ) )
123 122 fveqeq2d ⊢ ( 𝑗 = ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
124 123 ralbidv ⊢ ( 𝑗 = ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑒 ∈ dom ( iEdg ‘ 𝐺 ) ↦ ( ◡ ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑒 ) ) ) ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
125 121 124 anbi12d ⊢ ( 𝑗 = ( 𝑒 ∈ 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 ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
126 118 120 125 spcedv ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
127 126 ex ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐷 → ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
128 114 127 impbid ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ↔ ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐷 ) )
129 f1oeq1 ⊢ ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) = ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) → ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐷 ↔ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) )
130 110 129 mp1i ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) ) : 𝐸 –1-1-onto→ 𝐷 ↔ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) )
131 128 130 bitrd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ↔ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) )
132 131 pm5.32da ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) )
133 7 132 bitrd ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ 𝑋 ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) )