Metamath Proof Explorer

Theorem uspgrimprop

Description: An isomorphism of simple pseudographs is a bijection between their vertices that preserves adjacency, i.e. there is an edge in one graph connecting one or two vertices iff there is an edge in the other graph connecting the vertices which are the images of the vertices. (Contributed by AV, 27-Apr-2025)

Ref Expression
Hypotheses isusgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isusgrim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
isusgrim.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
isusgrim.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
Assertion uspgrimprop ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –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 1 2 3 4 isuspgrim0 ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) )
6 5 3expa ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) )
7 simprl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
8 imaeq2 ⊢ ( 𝑒 = { 𝑥 , 𝑦 } → ( 𝐹 “ 𝑒 ) = ( 𝐹 “ { 𝑥 , 𝑦 } ) )
9 eqidd ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) )
10 simpr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → { 𝑥 , 𝑦 } ∈ 𝐸 )
11 f1ofun ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → Fun 𝐹 )
12 zfpair2 ⊢ { 𝑥 , 𝑦 } ∈ V
13 funimaexg ⊢ ( ( Fun 𝐹 ∧ { 𝑥 , 𝑦 } ∈ V ) → ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ V )
14 11 12 13 sylancl ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ V )
15 14 adantr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ V )
16 8 9 10 15 fvmptd4 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ { 𝑥 , 𝑦 } ) = ( 𝐹 “ { 𝑥 , 𝑦 } ) )
17 16 ex ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → ( { 𝑥 , 𝑦 } ∈ 𝐸 → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ { 𝑥 , 𝑦 } ) = ( 𝐹 “ { 𝑥 , 𝑦 } ) ) )
18 17 adantr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ { 𝑥 , 𝑦 } ) = ( 𝐹 “ { 𝑥 , 𝑦 } ) ) )
19 18 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ { 𝑥 , 𝑦 } ) = ( 𝐹 “ { 𝑥 , 𝑦 } ) ) )
20 19 imp ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ { 𝑥 , 𝑦 } ) = ( 𝐹 “ { 𝑥 , 𝑦 } ) )
21 f1of ⊢ ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 → ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 ⟶ 𝐷 )
22 21 ad2antll ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) → ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 ⟶ 𝐷 )
23 ax-1 ⊢ ( ∅ ∉ 𝐷 → ( 𝐻 ∈ USPGraph → ∅ ∉ 𝐷 ) )
24 nnel ⊢ ( ¬ ∅ ∉ 𝐷 ↔ ∅ ∈ 𝐷 )
25 uspgruhgr ⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UHGraph )
26 uhgredgn0 ⊢ ( ( 𝐻 ∈ UHGraph ∧ ∅ ∈ ( Edg ‘ 𝐻 ) ) → ∅ ∈ ( 𝒫 ( Vtx ‘ 𝐻 ) ∖ { ∅ } ) )
27 25 26 sylan ⊢ ( ( 𝐻 ∈ USPGraph ∧ ∅ ∈ ( Edg ‘ 𝐻 ) ) → ∅ ∈ ( 𝒫 ( Vtx ‘ 𝐻 ) ∖ { ∅ } ) )
28 neldifsn ⊢ ¬ ∅ ∈ ( 𝒫 ( Vtx ‘ 𝐻 ) ∖ { ∅ } )
29 28 pm2.21i ⊢ ( ∅ ∈ ( 𝒫 ( Vtx ‘ 𝐻 ) ∖ { ∅ } ) → ∅ ∉ 𝐷 )
30 27 29 syl ⊢ ( ( 𝐻 ∈ USPGraph ∧ ∅ ∈ ( Edg ‘ 𝐻 ) ) → ∅ ∉ 𝐷 )
31 30 expcom ⊢ ( ∅ ∈ ( Edg ‘ 𝐻 ) → ( 𝐻 ∈ USPGraph → ∅ ∉ 𝐷 ) )
32 31 4 eleq2s ⊢ ( ∅ ∈ 𝐷 → ( 𝐻 ∈ USPGraph → ∅ ∉ 𝐷 ) )
33 24 32 sylbi ⊢ ( ¬ ∅ ∉ 𝐷 → ( 𝐻 ∈ USPGraph → ∅ ∉ 𝐷 ) )
34 23 33 pm2.61i ⊢ ( 𝐻 ∈ USPGraph → ∅ ∉ 𝐷 )
35 34 ad2antlr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) → ∅ ∉ 𝐷 )
36 22 35 jca ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 ⟶ 𝐷 ∧ ∅ ∉ 𝐷 ) )
37 36 adantr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 ⟶ 𝐷 ∧ ∅ ∉ 𝐷 ) )
38 feldmfvelcdm ⊢ ( ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 ⟶ 𝐷 ∧ ∅ ∉ 𝐷 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) )
39 37 38 syl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) )
40 39 biimpa ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ { 𝑥 , 𝑦 } ) ∈ 𝐷 )
41 20 40 eqeltrrd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 )
42 imaeq2 ⊢ ( 𝑧 = ( 𝐹 “ { 𝑥 , 𝑦 } ) → ( ◡ 𝐹 “ 𝑧 ) = ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) )
43 imaeq2 ⊢ ( 𝑒 = 𝑦 → ( 𝐹 “ 𝑒 ) = ( 𝐹 “ 𝑦 ) )
44 43 cbvmptv ⊢ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) )
45 f1oeq1 ⊢ ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ↔ ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 ) )
46 44 45 mp1i ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ↔ ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 ) )
47 imaeq2 ⊢ ( 𝑒 = 𝑥 → ( 𝐹 “ 𝑒 ) = ( 𝐹 “ 𝑥 ) )
48 47 cbvmptv ⊢ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ( 𝑥 ∈ 𝐸 ↦ ( 𝐹 “ 𝑥 ) )
49 simpr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
50 49 adantr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
51 uspgruhgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
52 uhgredgss ⊢ ( 𝐺 ∈ UHGraph → ( Edg ‘ 𝐺 ) ⊆ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
53 difss2 ⊢ ( ( Edg ‘ 𝐺 ) ⊆ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → ( Edg ‘ 𝐺 ) ⊆ 𝒫 ( Vtx ‘ 𝐺 ) )
54 51 52 53 3syl ⊢ ( 𝐺 ∈ USPGraph → ( Edg ‘ 𝐺 ) ⊆ 𝒫 ( Vtx ‘ 𝐺 ) )
55 1 pweqi ⊢ 𝒫 𝑉 = 𝒫 ( Vtx ‘ 𝐺 )
56 54 3 55 3sstr4g ⊢ ( 𝐺 ∈ USPGraph → 𝐸 ⊆ 𝒫 𝑉 )
57 56 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → 𝐸 ⊆ 𝒫 𝑉 )
58 57 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → 𝐸 ⊆ 𝒫 𝑉 )
59 f1ofo ⊢ ( ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 → ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –onto→ 𝐷 )
60 44 rneqi ⊢ ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ran ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) )
61 forn ⊢ ( ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –onto→ 𝐷 → ran ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) = 𝐷 )
62 60 61 eqtrid ⊢ ( ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –onto→ 𝐷 → ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = 𝐷 )
63 59 62 syl ⊢ ( ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 → ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = 𝐷 )
64 63 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = 𝐷 )
65 uhgredgss ⊢ ( 𝐻 ∈ UHGraph → ( Edg ‘ 𝐻 ) ⊆ ( 𝒫 ( Vtx ‘ 𝐻 ) ∖ { ∅ } ) )
66 difss2 ⊢ ( ( Edg ‘ 𝐻 ) ⊆ ( 𝒫 ( Vtx ‘ 𝐻 ) ∖ { ∅ } ) → ( Edg ‘ 𝐻 ) ⊆ 𝒫 ( Vtx ‘ 𝐻 ) )
67 25 65 66 3syl ⊢ ( 𝐻 ∈ USPGraph → ( Edg ‘ 𝐻 ) ⊆ 𝒫 ( Vtx ‘ 𝐻 ) )
68 2 pweqi ⊢ 𝒫 𝑊 = 𝒫 ( Vtx ‘ 𝐻 )
69 67 4 68 3sstr4g ⊢ ( 𝐻 ∈ USPGraph → 𝐷 ⊆ 𝒫 𝑊 )
70 69 adantl ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → 𝐷 ⊆ 𝒫 𝑊 )
71 70 ad2antrr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → 𝐷 ⊆ 𝒫 𝑊 )
72 64 71 eqsstrd ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ⊆ 𝒫 𝑊 )
73 1 fvexi ⊢ 𝑉 ∈ V
74 73 a1i ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → 𝑉 ∈ V )
75 48 50 58 72 74 mptcnfimad ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → ◡ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ( 𝑧 ∈ ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ↦ ( ◡ 𝐹 “ 𝑧 ) ) )
76 75 ex ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ( 𝑦 ∈ 𝐸 ↦ ( 𝐹 “ 𝑦 ) ) : 𝐸 –1-1-onto→ 𝐷 → ◡ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ( 𝑧 ∈ ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ↦ ( ◡ 𝐹 “ 𝑧 ) ) ) )
77 46 76 sylbid ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 → ◡ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ( 𝑧 ∈ ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ↦ ( ◡ 𝐹 “ 𝑧 ) ) ) )
78 77 impr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) → ◡ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ( 𝑧 ∈ ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ↦ ( ◡ 𝐹 “ 𝑧 ) ) )
79 78 ad2antrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) → ◡ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ( 𝑧 ∈ ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ↦ ( ◡ 𝐹 “ 𝑧 ) ) )
80 f1ofo ⊢ ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 → ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –onto→ 𝐷 )
81 forn ⊢ ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –onto→ 𝐷 → ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = 𝐷 )
82 81 eqcomd ⊢ ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –onto→ 𝐷 → 𝐷 = ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) )
83 80 82 syl ⊢ ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 → 𝐷 = ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) )
84 83 adantl ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → 𝐷 = ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) )
85 84 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → 𝐷 = ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) )
86 85 eleq2d ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ↔ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ) )
87 86 biimpa ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) → ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ ran ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) )
88 dff1o2 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ↔ ( 𝐹 Fn 𝑉 ∧ Fun ◡ 𝐹 ∧ ran 𝐹 = 𝑊 ) )
89 88 simp2bi ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → Fun ◡ 𝐹 )
90 89 adantr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → Fun ◡ 𝐹 )
91 90 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → Fun ◡ 𝐹 )
92 funimaexg ⊢ ( ( Fun ◡ 𝐹 ∧ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) → ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) ∈ V )
93 91 92 sylan ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) → ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) ∈ V )
94 42 79 87 93 fvmptd4 ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) → ( ◡ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) = ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) )
95 simplrr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 )
96 f1ocnvdm ⊢ ( ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ∧ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) → ( ◡ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) ∈ 𝐸 )
97 95 96 sylan ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) → ( ◡ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) ‘ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) ∈ 𝐸 )
98 94 97 eqeltrrd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) → ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) ∈ 𝐸 )
99 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 –1-1→ 𝑊 )
100 99 ad2antrl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) → 𝐹 : 𝑉 –1-1→ 𝑊 )
101 prssi ⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → { 𝑥 , 𝑦 } ⊆ 𝑉 )
102 f1imacnv ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ { 𝑥 , 𝑦 } ⊆ 𝑉 ) → ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) = { 𝑥 , 𝑦 } )
103 100 101 102 syl2an ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) = { 𝑥 , 𝑦 } )
104 103 eqcomd ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → { 𝑥 , 𝑦 } = ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) )
105 104 eleq1d ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) ∈ 𝐸 ) )
106 105 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ ( ◡ 𝐹 “ ( 𝐹 “ { 𝑥 , 𝑦 } ) ) ∈ 𝐸 ) )
107 98 106 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) ∧ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) → { 𝑥 , 𝑦 } ∈ 𝐸 )
108 41 107 impbida ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ) )
109 f1ofn ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 Fn 𝑉 )
110 109 ad2antrl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) → 𝐹 Fn 𝑉 )
111 110 anim1i ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
112 3anass ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ↔ ( 𝐹 Fn 𝑉 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) )
113 111 112 sylibr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) )
114 fnimapr ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝐹 “ { 𝑥 , 𝑦 } ) = { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } )
115 113 114 syl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( 𝐹 “ { 𝑥 , 𝑦 } ) = { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } )
116 115 eleq1d ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( ( 𝐹 “ { 𝑥 , 𝑦 } ) ∈ 𝐷 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) )
117 108 116 bitrd ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) )
118 117 ralrimivva ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) )
119 7 118 jca ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) )
120 119 ex ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ) )
121 120 adantr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ) )
122 6 121 sylbid ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ) )
123 122 syldbl2 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) )
124 123 ex ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ) )