Metamath Proof Explorer

Theorem isomuspgr

Description: The isomorphy relation for two simple pseudographs. This corresponds to the definition in Bollobas p. 3. (Contributed by AV, 1-Dec-2022)

Ref Expression
Hypotheses isomushgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐴 )
isomushgr.w ⊢ 𝑊 = ( Vtx ‘ 𝐵 )
isomushgr.e ⊢ 𝐸 = ( Edg ‘ 𝐴 )
isomushgr.k ⊢ 𝐾 = ( Edg ‘ 𝐵 )
Assertion isomuspgr ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )

Proof

Step Hyp Ref Expression
1 isomushgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2 isomushgr.w ⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3 isomushgr.e ⊢ 𝐸 = ( Edg ‘ 𝐴 )
4 isomushgr.k ⊢ 𝐾 = ( Edg ‘ 𝐵 )
5 uspgrushgr ⊢ ( 𝐴 ∈ USPGraph → 𝐴 ∈ USHGraph )
6 uspgrushgr ⊢ ( 𝐵 ∈ USPGraph → 𝐵 ∈ USHGraph )
7 1 2 3 4 isomushgr ⊢ ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
8 5 6 7 syl2an ⊢ ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
9 imaeq2 ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( 𝑓 “ 𝑒 ) = ( 𝑓 “ { 𝑎 , 𝑏 } ) )
10 fveq2 ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( 𝑔 ‘ 𝑒 ) = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) )
11 9 10 eqeq12d ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ( 𝑓 “ { 𝑎 , 𝑏 } ) = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ) )
12 11 rspccv ⊢ ( ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 → ( 𝑓 “ { 𝑎 , 𝑏 } ) = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ) )
13 12 adantl ⊢ ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 → ( 𝑓 “ { 𝑎 , 𝑏 } ) = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ) )
14 13 imp ⊢ ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( 𝑓 “ { 𝑎 , 𝑏 } ) = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) )
15 f1ofn ⊢ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 → 𝑓 Fn 𝑉 )
16 15 ad3antlr ⊢ ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑓 Fn 𝑉 )
17 simprl ⊢ ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑎 ∈ 𝑉 )
18 simprr ⊢ ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑏 ∈ 𝑉 )
19 fnimapr ⊢ ( ( 𝑓 Fn 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑓 “ { 𝑎 , 𝑏 } ) = { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } )
20 16 17 18 19 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑓 “ { 𝑎 , 𝑏 } ) = { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } )
21 20 eqeq1d ⊢ ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( ( 𝑓 “ { 𝑎 , 𝑏 } ) = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ) )
22 21 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ( ( 𝑓 “ { 𝑎 , 𝑏 } ) = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ) )
23 22 adantr ⊢ ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( ( 𝑓 “ { 𝑎 , 𝑏 } ) = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ) )
24 f1of ⊢ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 → 𝑔 : 𝐸 ⟶ 𝐾 )
25 24 ad3antlr ⊢ ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → 𝑔 : 𝐸 ⟶ 𝐾 )
26 25 ffvelrnda ⊢ ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ∈ 𝐾 )
27 eleq1 ⊢ ( { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) → ( { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ↔ ( 𝑔 ‘ { 𝑎 , 𝑏 } ) ∈ 𝐾 ) )
28 26 27 syl5ibrcom ⊢ ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) → { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) )
29 23 28 sylbid ⊢ ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( ( 𝑓 “ { 𝑎 , 𝑏 } ) = ( 𝑔 ‘ { 𝑎 , 𝑏 } ) → { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) )
30 14 29 mpd ⊢ ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 )
31 30 exp41 ⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 → { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )
32 31 com23 ⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑔 : 𝐸 –1-1-onto→ 𝐾 ) → ( ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 → { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )
33 32 impr ⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 → { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) )
34 33 imp ⊢ ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 → { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) )
35 1 2 3 4 isomuspgrlem1 ⊢ ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
36 34 35 impbid ⊢ ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) )
37 36 ralrimivva ⊢ ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) )
38 37 ex ⊢ ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) → ( ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) )
39 38 exlimdv ⊢ ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) )
40 1 2 3 4 isomuspgrlem2 ⊢ ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) → ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
41 39 40 impbid ⊢ ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) )
42 41 pm5.32da ⊢ ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → ( ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )
43 42 exbidv ⊢ ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → ( ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )
44 8 43 bitrd ⊢ ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )