# 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𝑊 ∧ ∀ 𝑎𝑉𝑏𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ) ) )