Metamath Proof Explorer

Theorem isomuspgrlem1

Description: Lemma 1 for isomuspgr . (Contributed by AV, 29-Nov-2022)

Ref Expression
Hypotheses isomushgr.v 𝑉 = ( Vtx ‘ 𝐴 )
isomushgr.w 𝑊 = ( Vtx ‘ 𝐵 )
isomushgr.e 𝐸 = ( Edg ‘ 𝐴 )
isomushgr.k 𝐾 = ( Edg ‘ 𝐵 )
Assertion isomuspgrlem1 ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸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 simpl ( ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) → 𝑔 : 𝐸1-1-onto𝐾 )
6 5 ad2antlr ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) → 𝑔 : 𝐸1-1-onto𝐾 )
7 f1ocnvdm ( ( 𝑔 : 𝐸1-1-onto𝐾 ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) → ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 )
8 6 7 sylan ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) → ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 )
9 uspgrupgr ( 𝐴 ∈ USPGraph → 𝐴 ∈ UPGraph )
10 9 adantr ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → 𝐴 ∈ UPGraph )
11 10 ad4antr ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) → 𝐴 ∈ UPGraph )
12 1 3 upgredg ( ( 𝐴 ∈ UPGraph ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) → ∃ 𝑥𝑉𝑦𝑉 ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } )
13 11 12 sylan ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) → ∃ 𝑥𝑉𝑦𝑉 ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } )
14 eleq1 ( ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } → ( ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ↔ { 𝑥 , 𝑦 } ∈ 𝐸 ) )
15 14 biimpd ( ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } → ( ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 → { 𝑥 , 𝑦 } ∈ 𝐸 ) )
16 15 com12 ( ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 → ( ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } → { 𝑥 , 𝑦 } ∈ 𝐸 ) )
17 16 ad2antlr ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } → { 𝑥 , 𝑦 } ∈ 𝐸 ) )
18 17 imp ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } ) → { 𝑥 , 𝑦 } ∈ 𝐸 )
19 5 ad6antlr ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → 𝑔 : 𝐸1-1-onto𝐾 )
20 simpr ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → { 𝑥 , 𝑦 } ∈ 𝐸 )
21 simpr ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) → { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 )
22 21 ad5ant12 ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 )
23 19 20 22 3jca ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( 𝑔 : 𝐸1-1-onto𝐾 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) )
24 f1ocnvfvb ( ( 𝑔 : 𝐸1-1-onto𝐾 ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) → ( ( 𝑔 ‘ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ↔ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } ) )
25 23 24 syl ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( ( 𝑔 ‘ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ↔ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } ) )
26 imaeq2 ( 𝑒 = { 𝑥 , 𝑦 } → ( 𝑓𝑒 ) = ( 𝑓 “ { 𝑥 , 𝑦 } ) )
27 fveq2 ( 𝑒 = { 𝑥 , 𝑦 } → ( 𝑔𝑒 ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) )
28 26 27 eqeq12d ( 𝑒 = { 𝑥 , 𝑦 } → ( ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ↔ ( 𝑓 “ { 𝑥 , 𝑦 } ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) ) )
29 28 rspccv ( ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 → ( 𝑓 “ { 𝑥 , 𝑦 } ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) ) )
30 29 adantl ( ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 → ( 𝑓 “ { 𝑥 , 𝑦 } ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) ) )
31 30 adantl ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 → ( 𝑓 “ { 𝑥 , 𝑦 } ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) ) )
32 31 ad4antr ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 → ( 𝑓 “ { 𝑥 , 𝑦 } ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) ) )
33 32 imp ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( 𝑓 “ { 𝑥 , 𝑦 } ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) )
34 eqeq1 ( ( 𝑔 ‘ { 𝑥 , 𝑦 } ) = ( 𝑓 “ { 𝑥 , 𝑦 } ) → ( ( 𝑔 ‘ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ↔ ( 𝑓 “ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) )
35 34 eqcoms ( ( 𝑓 “ { 𝑥 , 𝑦 } ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) → ( ( 𝑔 ‘ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ↔ ( 𝑓 “ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) )
36 35 adantl ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ∧ ( 𝑓 “ { 𝑥 , 𝑦 } ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) ) → ( ( 𝑔 ‘ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ↔ ( 𝑓 “ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) )
37 f1ofn ( 𝑓 : 𝑉1-1-onto𝑊𝑓 Fn 𝑉 )
38 37 ad6antlr ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → 𝑓 Fn 𝑉 )
39 simpl ( ( 𝑥𝑉𝑦𝑉 ) → 𝑥𝑉 )
40 39 adantl ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → 𝑥𝑉 )
41 simpr ( ( 𝑥𝑉𝑦𝑉 ) → 𝑦𝑉 )
42 41 adantl ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → 𝑦𝑉 )
43 38 40 42 3jca ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑓 Fn 𝑉𝑥𝑉𝑦𝑉 ) )
44 43 adantr ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( 𝑓 Fn 𝑉𝑥𝑉𝑦𝑉 ) )
45 fnimapr ( ( 𝑓 Fn 𝑉𝑥𝑉𝑦𝑉 ) → ( 𝑓 “ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } )
46 44 45 syl ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( 𝑓 “ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } )
47 46 eqeq1d ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( ( 𝑓 “ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ↔ { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) )
48 fvex ( 𝑓𝑥 ) ∈ V
49 fvex ( 𝑓𝑦 ) ∈ V
50 fvex ( 𝑓𝑎 ) ∈ V
51 fvex ( 𝑓𝑏 ) ∈ V
52 48 49 50 51 preq12b ( { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ↔ ( ( ( 𝑓𝑥 ) = ( 𝑓𝑎 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑏 ) ) ∨ ( ( 𝑓𝑥 ) = ( 𝑓𝑏 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑎 ) ) ) )
53 f1of1 ( 𝑓 : 𝑉1-1-onto𝑊𝑓 : 𝑉1-1𝑊 )
54 simpl ( ( 𝑎𝑉𝑏𝑉 ) → 𝑎𝑉 )
55 54 39 anim12ci ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑥𝑉𝑎𝑉 ) )
56 f1veqaeq ( ( 𝑓 : 𝑉1-1𝑊 ∧ ( 𝑥𝑉𝑎𝑉 ) ) → ( ( 𝑓𝑥 ) = ( 𝑓𝑎 ) → 𝑥 = 𝑎 ) )
57 53 55 56 syl2anr ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → ( ( 𝑓𝑥 ) = ( 𝑓𝑎 ) → 𝑥 = 𝑎 ) )
58 simpr ( ( 𝑎𝑉𝑏𝑉 ) → 𝑏𝑉 )
59 58 41 anim12ci ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑦𝑉𝑏𝑉 ) )
60 f1veqaeq ( ( 𝑓 : 𝑉1-1𝑊 ∧ ( 𝑦𝑉𝑏𝑉 ) ) → ( ( 𝑓𝑦 ) = ( 𝑓𝑏 ) → 𝑦 = 𝑏 ) )
61 53 59 60 syl2anr ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → ( ( 𝑓𝑦 ) = ( 𝑓𝑏 ) → 𝑦 = 𝑏 ) )
62 57 61 anim12d ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → ( ( ( 𝑓𝑥 ) = ( 𝑓𝑎 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑏 ) ) → ( 𝑥 = 𝑎𝑦 = 𝑏 ) ) )
63 62 impcom ( ( ( ( 𝑓𝑥 ) = ( 𝑓𝑎 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑏 ) ) ∧ ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ) → ( 𝑥 = 𝑎𝑦 = 𝑏 ) )
64 63 orcd ( ( ( ( 𝑓𝑥 ) = ( 𝑓𝑎 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑏 ) ) ∧ ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ) → ( ( 𝑥 = 𝑎𝑦 = 𝑏 ) ∨ ( 𝑥 = 𝑏𝑦 = 𝑎 ) ) )
65 64 ex ( ( ( 𝑓𝑥 ) = ( 𝑓𝑎 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑏 ) ) → ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → ( ( 𝑥 = 𝑎𝑦 = 𝑏 ) ∨ ( 𝑥 = 𝑏𝑦 = 𝑎 ) ) ) )
66 58 39 anim12ci ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑥𝑉𝑏𝑉 ) )
67 f1veqaeq ( ( 𝑓 : 𝑉1-1𝑊 ∧ ( 𝑥𝑉𝑏𝑉 ) ) → ( ( 𝑓𝑥 ) = ( 𝑓𝑏 ) → 𝑥 = 𝑏 ) )
68 53 66 67 syl2anr ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → ( ( 𝑓𝑥 ) = ( 𝑓𝑏 ) → 𝑥 = 𝑏 ) )
69 54 41 anim12ci ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( 𝑦𝑉𝑎𝑉 ) )
70 f1veqaeq ( ( 𝑓 : 𝑉1-1𝑊 ∧ ( 𝑦𝑉𝑎𝑉 ) ) → ( ( 𝑓𝑦 ) = ( 𝑓𝑎 ) → 𝑦 = 𝑎 ) )
71 53 69 70 syl2anr ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → ( ( 𝑓𝑦 ) = ( 𝑓𝑎 ) → 𝑦 = 𝑎 ) )
72 68 71 anim12d ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → ( ( ( 𝑓𝑥 ) = ( 𝑓𝑏 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑎 ) ) → ( 𝑥 = 𝑏𝑦 = 𝑎 ) ) )
73 72 impcom ( ( ( ( 𝑓𝑥 ) = ( 𝑓𝑏 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑎 ) ) ∧ ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ) → ( 𝑥 = 𝑏𝑦 = 𝑎 ) )
74 73 olcd ( ( ( ( 𝑓𝑥 ) = ( 𝑓𝑏 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑎 ) ) ∧ ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ) → ( ( 𝑥 = 𝑎𝑦 = 𝑏 ) ∨ ( 𝑥 = 𝑏𝑦 = 𝑎 ) ) )
75 74 ex ( ( ( 𝑓𝑥 ) = ( 𝑓𝑏 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑎 ) ) → ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → ( ( 𝑥 = 𝑎𝑦 = 𝑏 ) ∨ ( 𝑥 = 𝑏𝑦 = 𝑎 ) ) ) )
76 65 75 jaoi ( ( ( ( 𝑓𝑥 ) = ( 𝑓𝑎 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑏 ) ) ∨ ( ( 𝑓𝑥 ) = ( 𝑓𝑏 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑎 ) ) ) → ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → ( ( 𝑥 = 𝑎𝑦 = 𝑏 ) ∨ ( 𝑥 = 𝑏𝑦 = 𝑎 ) ) ) )
77 vex 𝑥 ∈ V
78 vex 𝑦 ∈ V
79 vex 𝑎 ∈ V
80 vex 𝑏 ∈ V
81 77 78 79 80 preq12b ( { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ↔ ( ( 𝑥 = 𝑎𝑦 = 𝑏 ) ∨ ( 𝑥 = 𝑏𝑦 = 𝑎 ) ) )
82 76 81 syl6ibr ( ( ( ( 𝑓𝑥 ) = ( 𝑓𝑎 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑏 ) ) ∨ ( ( 𝑓𝑥 ) = ( 𝑓𝑏 ) ∧ ( 𝑓𝑦 ) = ( 𝑓𝑎 ) ) ) → ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) )
83 52 82 sylbi ( { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) )
84 83 com12 ( ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) → ( { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) )
85 84 expcom ( 𝑓 : 𝑉1-1-onto𝑊 → ( ( ( 𝑎𝑉𝑏𝑉 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) )
86 85 expd ( 𝑓 : 𝑉1-1-onto𝑊 → ( ( 𝑎𝑉𝑏𝑉 ) → ( ( 𝑥𝑉𝑦𝑉 ) → ( { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ) )
87 86 ad2antlr ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) → ( ( 𝑎𝑉𝑏𝑉 ) → ( ( 𝑥𝑉𝑦𝑉 ) → ( { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) ) )
88 87 imp ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) → ( ( 𝑥𝑉𝑦𝑉 ) → ( { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) )
89 88 adantr ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) → ( ( 𝑥𝑉𝑦𝑉 ) → ( { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) )
90 89 adantr ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) → ( ( 𝑥𝑉𝑦𝑉 ) → ( { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } ) ) )
91 90 imp31 ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } )
92 91 eleq1d ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { 𝑎 , 𝑏 } ∈ 𝐸 ) )
93 92 biimpd ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
94 93 impancom ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( { ( 𝑓𝑥 ) , ( 𝑓𝑦 ) } = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
95 47 94 sylbid ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( ( 𝑓 “ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
96 95 adantr ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ∧ ( 𝑓 “ { 𝑥 , 𝑦 } ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) ) → ( ( 𝑓 “ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
97 36 96 sylbid ( ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) ∧ ( 𝑓 “ { 𝑥 , 𝑦 } ) = ( 𝑔 ‘ { 𝑥 , 𝑦 } ) ) → ( ( 𝑔 ‘ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
98 33 97 mpdan ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( ( 𝑔 ‘ { 𝑥 , 𝑦 } ) = { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
99 25 98 sylbird ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ { 𝑥 , 𝑦 } ∈ 𝐸 ) → ( ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
100 99 impancom ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
101 18 100 mpd ( ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
102 101 ex ( ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) ∧ ( 𝑥𝑉𝑦𝑉 ) ) → ( ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
103 102 rexlimdvva ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) → ( ∃ 𝑥𝑉𝑦𝑉 ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) = { 𝑥 , 𝑦 } → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
104 13 103 mpd ( ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑔 ‘ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ) ∈ 𝐸 ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
105 8 104 mpdan ( ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
106 105 ex ( ( ( ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) ∧ 𝑓 : 𝑉1-1-onto𝑊 ) ∧ ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ∧ ( 𝑎𝑉𝑏𝑉 ) ) → ( { ( 𝑓𝑎 ) , ( 𝑓𝑏 ) } ∈ 𝐾 → { 𝑎 , 𝑏 } ∈ 𝐸 ) )