Metamath Proof Explorer

Theorem isuspgrimlem

Description: Lemma for isuspgrim . (Contributed by AV, 27-Apr-2025)

Ref Expression
Hypotheses isusgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isusgrim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
isusgrim.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
isusgrim.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
Assertion isuspgrimlem ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –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 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
6 5 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → 𝐺 ∈ UPGraph )
7 6 adantr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → 𝐺 ∈ UPGraph )
8 7 adantr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → 𝐺 ∈ UPGraph )
9 1 3 upgredg ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑒 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑒 = { 𝑎 , 𝑏 } )
10 8 9 sylan ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ 𝑒 ∈ 𝐸 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑒 = { 𝑎 , 𝑏 } )
11 preq12 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → { 𝑥 , 𝑦 } = { 𝑎 , 𝑏 } )
12 11 eleq1d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { 𝑎 , 𝑏 } ∈ 𝐸 ) )
13 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
14 13 adantr ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
15 fveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑏 ) )
16 15 adantl ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑏 ) )
17 14 16 preq12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } )
18 17 eleq1d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐷 ) )
19 12 18 bibi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐷 ) ) )
20 19 rspc2gv ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐷 ) ) )
21 20 com12 ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐷 ) ) )
22 21 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐷 ) ) )
23 22 imp ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐷 ) )
24 f1ofn ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 Fn 𝑉 )
25 24 ad3antlr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝐹 Fn 𝑉 )
26 simprl ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑎 ∈ 𝑉 )
27 simpr ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
28 27 adantl ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → 𝑏 ∈ 𝑉 )
29 fnimapr ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝐹 “ { 𝑎 , 𝑏 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } )
30 25 26 28 29 syl3anc ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝐹 “ { 𝑎 , 𝑏 } ) = { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } )
31 30 eqcomd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } = ( 𝐹 “ { 𝑎 , 𝑏 } ) )
32 31 eleq1d ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐷 ↔ ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ 𝐷 ) )
33 23 32 bitrd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ 𝐷 ) )
34 33 adantr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ 𝐷 ) )
35 34 biimpd ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 → ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ 𝐷 ) )
36 eleq1 ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( 𝑒 ∈ 𝐸 ↔ { 𝑎 , 𝑏 } ∈ 𝐸 ) )
37 imaeq2 ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( 𝐹 “ 𝑒 ) = ( 𝐹 “ { 𝑎 , 𝑏 } ) )
38 37 eleq1d ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( ( 𝐹 “ 𝑒 ) ∈ 𝐷 ↔ ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ 𝐷 ) )
39 36 38 imbi12d ⊢ ( 𝑒 = { 𝑎 , 𝑏 } → ( ( 𝑒 ∈ 𝐸 → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝐸 → ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ 𝐷 ) ) )
40 39 adantl ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( ( 𝑒 ∈ 𝐸 → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝐸 → ( 𝐹 “ { 𝑎 , 𝑏 } ) ∈ 𝐷 ) ) )
41 35 40 mpbird ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ 𝑒 = { 𝑎 , 𝑏 } ) → ( 𝑒 ∈ 𝐸 → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) )
42 41 exp31 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑒 = { 𝑎 , 𝑏 } → ( 𝑒 ∈ 𝐸 → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) ) ) )
43 42 com23 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( 𝑒 = { 𝑎 , 𝑏 } → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑒 ∈ 𝐸 → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) ) ) )
44 43 com24 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( 𝑒 ∈ 𝐸 → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑒 = { 𝑎 , 𝑏 } → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) ) ) )
45 44 imp ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ 𝑒 ∈ 𝐸 ) → ( ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) → ( 𝑒 = { 𝑎 , 𝑏 } → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) ) )
46 45 rexlimdvv ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ 𝑒 ∈ 𝐸 ) → ( ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑒 = { 𝑎 , 𝑏 } → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) )
47 10 46 mpd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝐹 “ 𝑒 ) ∈ 𝐷 )
48 47 ex ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( 𝑒 ∈ 𝐸 → ( 𝐹 “ 𝑒 ) ∈ 𝐷 ) )
49 48 ralrimiv ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) ∈ 𝐷 )
50 uspgrupgr ⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UPGraph )
51 50 ad3antlr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → 𝐻 ∈ UPGraph )
52 2 4 upgredg ⊢ ( ( 𝐻 ∈ UPGraph ∧ 𝑑 ∈ 𝐷 ) → ∃ 𝑎 ∈ 𝑊 ∃ 𝑏 ∈ 𝑊 𝑑 = { 𝑎 , 𝑏 } )
53 51 52 sylan ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ 𝑑 ∈ 𝐷 ) → ∃ 𝑎 ∈ 𝑊 ∃ 𝑏 ∈ 𝑊 𝑑 = { 𝑎 , 𝑏 } )
54 f1ofo ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 –onto→ 𝑊 )
55 foelrn ⊢ ( ( 𝐹 : 𝑉 –onto→ 𝑊 ∧ 𝑎 ∈ 𝑊 ) → ∃ 𝑚 ∈ 𝑉 𝑎 = ( 𝐹 ‘ 𝑚 ) )
56 55 ex ⊢ ( 𝐹 : 𝑉 –onto→ 𝑊 → ( 𝑎 ∈ 𝑊 → ∃ 𝑚 ∈ 𝑉 𝑎 = ( 𝐹 ‘ 𝑚 ) ) )
57 foelrn ⊢ ( ( 𝐹 : 𝑉 –onto→ 𝑊 ∧ 𝑏 ∈ 𝑊 ) → ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) )
58 57 ex ⊢ ( 𝐹 : 𝑉 –onto→ 𝑊 → ( 𝑏 ∈ 𝑊 → ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) ) )
59 56 58 anim12d ⊢ ( 𝐹 : 𝑉 –onto→ 𝑊 → ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) → ( ∃ 𝑚 ∈ 𝑉 𝑎 = ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) ) ) )
60 54 59 syl ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) → ( ∃ 𝑚 ∈ 𝑉 𝑎 = ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) ) ) )
61 60 adantl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) → ( ∃ 𝑚 ∈ 𝑉 𝑎 = ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) ) ) )
62 61 adantr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) → ( ∃ 𝑚 ∈ 𝑉 𝑎 = ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) ) ) )
63 62 imp ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( ∃ 𝑚 ∈ 𝑉 𝑎 = ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) ) )
64 preq12 ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑚 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑛 ) ) → { 𝑎 , 𝑏 } = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
65 64 eqeq2d ⊢ ( ( 𝑎 = ( 𝐹 ‘ 𝑚 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑛 ) ) → ( 𝑑 = { 𝑎 , 𝑏 } ↔ 𝑑 = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ) )
66 65 ancoms ⊢ ( ( 𝑏 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑎 = ( 𝐹 ‘ 𝑚 ) ) → ( 𝑑 = { 𝑎 , 𝑏 } ↔ 𝑑 = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ) )
67 66 adantl ⊢ ( ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑛 ∈ 𝑉 ) ∧ ( 𝑏 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑎 = ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝑑 = { 𝑎 , 𝑏 } ↔ 𝑑 = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ) )
68 preq12 ⊢ ( ( 𝑥 = 𝑚 ∧ 𝑦 = 𝑛 ) → { 𝑥 , 𝑦 } = { 𝑚 , 𝑛 } )
69 68 eleq1d ⊢ ( ( 𝑥 = 𝑚 ∧ 𝑦 = 𝑛 ) → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { 𝑚 , 𝑛 } ∈ 𝐸 ) )
70 fveq2 ⊢ ( 𝑥 = 𝑚 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑚 ) )
71 70 adantr ⊢ ( ( 𝑥 = 𝑚 ∧ 𝑦 = 𝑛 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑚 ) )
72 fveq2 ⊢ ( 𝑦 = 𝑛 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑛 ) )
73 72 adantl ⊢ ( ( 𝑥 = 𝑚 ∧ 𝑦 = 𝑛 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑛 ) )
74 71 73 preq12d ⊢ ( ( 𝑥 = 𝑚 ∧ 𝑦 = 𝑛 ) → { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
75 74 eleq1d ⊢ ( ( 𝑥 = 𝑚 ∧ 𝑦 = 𝑛 ) → ( { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 ) )
76 69 75 bibi12d ⊢ ( ( 𝑥 = 𝑚 ∧ 𝑦 = 𝑛 ) → ( ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ↔ ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 ) ) )
77 76 rspc2gv ⊢ ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) → ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 ) ) )
78 77 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) → ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 ) ) )
79 24 adantl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → 𝐹 Fn 𝑉 )
80 79 anim1i ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) )
81 3anass ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ↔ ( 𝐹 Fn 𝑉 ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) )
82 80 81 sylibr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) )
83 fnimapr ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( 𝐹 “ { 𝑚 , 𝑛 } ) = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
84 82 83 syl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐹 “ { 𝑚 , 𝑛 } ) = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
85 84 eqcomd ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ { 𝑚 , 𝑛 } ) )
86 simpr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 ) ) → ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 ) )
87 simpr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) → { 𝑚 , 𝑛 } ∈ 𝐸 )
88 reueq ⊢ ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ ∃! 𝑒 ∈ 𝐸 𝑒 = { 𝑚 , 𝑛 } )
89 87 88 sylib ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) → ∃! 𝑒 ∈ 𝐸 𝑒 = { 𝑚 , 𝑛 } )
90 eqcom ⊢ ( { 𝑚 , 𝑛 } = 𝑒 ↔ 𝑒 = { 𝑚 , 𝑛 } )
91 90 reubii ⊢ ( ∃! 𝑒 ∈ 𝐸 { 𝑚 , 𝑛 } = 𝑒 ↔ ∃! 𝑒 ∈ 𝐸 𝑒 = { 𝑚 , 𝑛 } )
92 89 91 sylibr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) → ∃! 𝑒 ∈ 𝐸 { 𝑚 , 𝑛 } = 𝑒 )
93 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 –1-1→ 𝑊 )
94 93 adantl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → 𝐹 : 𝑉 –1-1→ 𝑊 )
95 94 ad5ant12 ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) ∧ 𝑒 ∈ 𝐸 ) → 𝐹 : 𝑉 –1-1→ 𝑊 )
96 prssi ⊢ ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → { 𝑚 , 𝑛 } ⊆ 𝑉 )
97 96 ad3antlr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) ∧ 𝑒 ∈ 𝐸 ) → { 𝑚 , 𝑛 } ⊆ 𝑉 )
98 uspgruhgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
99 98 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → 𝐺 ∈ UHGraph )
100 99 ad5ant12 ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) → 𝐺 ∈ UHGraph )
101 3 eleq2i ⊢ ( 𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ( Edg ‘ 𝐺 ) )
102 101 biimpi ⊢ ( 𝑒 ∈ 𝐸 → 𝑒 ∈ ( Edg ‘ 𝐺 ) )
103 edguhgr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) )
104 1 pweqi ⊢ 𝒫 𝑉 = 𝒫 ( Vtx ‘ 𝐺 )
105 103 104 eleqtrrdi ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → 𝑒 ∈ 𝒫 𝑉 )
106 100 102 105 syl2an ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝒫 𝑉 )
107 106 elpwid ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ⊆ 𝑉 )
108 f1imaeq ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( { 𝑚 , 𝑛 } ⊆ 𝑉 ∧ 𝑒 ⊆ 𝑉 ) ) → ( ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ↔ { 𝑚 , 𝑛 } = 𝑒 ) )
109 95 97 107 108 syl12anc ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) ∧ 𝑒 ∈ 𝐸 ) → ( ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ↔ { 𝑚 , 𝑛 } = 𝑒 ) )
110 109 reubidva ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) → ( ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ↔ ∃! 𝑒 ∈ 𝐸 { 𝑚 , 𝑛 } = 𝑒 ) )
111 92 110 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ { 𝑚 , 𝑛 } ∈ 𝐸 ) → ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) )
112 111 ex ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( { 𝑚 , 𝑛 } ∈ 𝐸 → ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ) )
113 112 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 ) ) → ( { 𝑚 , 𝑛 } ∈ 𝐸 → ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ) )
114 86 113 sylbird ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 ) ) → ( ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ) )
115 114 ex ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 ) → ( ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ) ) )
116 eleq1 ⊢ ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ { 𝑚 , 𝑛 } ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 ↔ ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 ) )
117 116 bibi2d ⊢ ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ { 𝑚 , 𝑛 } ) → ( ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 ) ↔ ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 ) ) )
118 eqeq1 ⊢ ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ { 𝑚 , 𝑛 } ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ↔ ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ) )
119 118 reubidv ⊢ ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ { 𝑚 , 𝑛 } ) → ( ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ↔ ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ) )
120 116 119 imbi12d ⊢ ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ { 𝑚 , 𝑛 } ) → ( ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) ↔ ( ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ) ) )
121 117 120 imbi12d ⊢ ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ { 𝑚 , 𝑛 } ) → ( ( ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) ) ↔ ( ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 ) → ( ( 𝐹 “ { 𝑚 , 𝑛 } ) ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 ( 𝐹 “ { 𝑚 , 𝑛 } ) = ( 𝐹 “ 𝑒 ) ) ) ) )
122 115 121 syl5ibrcom ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ { 𝑚 , 𝑛 } ) → ( ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) ) ) )
123 85 122 mpd ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) ) )
124 78 123 syld ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) ) )
125 124 impancom ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) ) )
126 125 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) ) )
127 126 impl ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑛 ∈ 𝑉 ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) )
128 eleq1 ⊢ ( 𝑑 = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } → ( 𝑑 ∈ 𝐷 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 ) )
129 eqeq1 ⊢ ( 𝑑 = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } → ( 𝑑 = ( 𝐹 “ 𝑒 ) ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) )
130 129 reubidv ⊢ ( 𝑑 = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } → ( ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ↔ ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) )
131 128 130 imbi12d ⊢ ( 𝑑 = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } → ( ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ↔ ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } = ( 𝐹 “ 𝑒 ) ) ) )
132 127 131 syl5ibrcom ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑛 ∈ 𝑉 ) → ( 𝑑 = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } → ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) )
133 132 adantr ⊢ ( ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑛 ∈ 𝑉 ) ∧ ( 𝑏 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑎 = ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝑑 = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } → ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) )
134 67 133 sylbid ⊢ ( ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑛 ∈ 𝑉 ) ∧ ( 𝑏 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑎 = ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝑑 = { 𝑎 , 𝑏 } → ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) )
135 134 exp32 ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑛 ∈ 𝑉 ) → ( 𝑏 = ( 𝐹 ‘ 𝑛 ) → ( 𝑎 = ( 𝐹 ‘ 𝑚 ) → ( 𝑑 = { 𝑎 , 𝑏 } → ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) ) ) )
136 135 rexlimdva ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) → ( ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) → ( 𝑎 = ( 𝐹 ‘ 𝑚 ) → ( 𝑑 = { 𝑎 , 𝑏 } → ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) ) ) )
137 136 com23 ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) → ( 𝑎 = ( 𝐹 ‘ 𝑚 ) → ( ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) → ( 𝑑 = { 𝑎 , 𝑏 } → ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) ) ) )
138 137 rexlimdva ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( ∃ 𝑚 ∈ 𝑉 𝑎 = ( 𝐹 ‘ 𝑚 ) → ( ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) → ( 𝑑 = { 𝑎 , 𝑏 } → ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) ) ) )
139 138 impd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( ( ∃ 𝑚 ∈ 𝑉 𝑎 = ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ 𝑉 𝑏 = ( 𝐹 ‘ 𝑛 ) ) → ( 𝑑 = { 𝑎 , 𝑏 } → ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) ) )
140 63 139 mpd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝑑 = { 𝑎 , 𝑏 } → ( 𝑑 ∈ 𝐷 → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) )
141 140 com23 ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) ) → ( 𝑑 ∈ 𝐷 → ( 𝑑 = { 𝑎 , 𝑏 } → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) )
142 141 impancom ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ 𝑑 ∈ 𝐷 ) → ( ( 𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊 ) → ( 𝑑 = { 𝑎 , 𝑏 } → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) ) )
143 142 rexlimdvv ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ 𝑑 ∈ 𝐷 ) → ( ∃ 𝑎 ∈ 𝑊 ∃ 𝑏 ∈ 𝑊 𝑑 = { 𝑎 , 𝑏 } → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) )
144 53 143 mpd ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) ∧ 𝑑 ∈ 𝐷 ) → ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) )
145 144 ralrimiva ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ∀ 𝑑 ∈ 𝐷 ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) )
146 eqid ⊢ ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) = ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) )
147 146 f1ompt ⊢ ( ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 ↔ ( ∀ 𝑒 ∈ 𝐸 ( 𝐹 “ 𝑒 ) ∈ 𝐷 ∧ ∀ 𝑑 ∈ 𝐷 ∃! 𝑒 ∈ 𝐸 𝑑 = ( 𝐹 “ 𝑒 ) ) )
148 49 145 147 sylanbrc ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ 𝑉 ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) } ∈ 𝐷 ) ) → ( 𝑒 ∈ 𝐸 ↦ ( 𝐹 “ 𝑒 ) ) : 𝐸 –1-1-onto→ 𝐷 )