# Metamath Proof Explorer

## Theorem isomuspgrlem2c

Description: Lemma 3 for isomuspgrlem2 . (Contributed by AV, 29-Nov-2022)

Ref Expression
Hypotheses isomushgr.v 𝑉 = ( Vtx ‘ 𝐴 )
isomushgr.w 𝑊 = ( Vtx ‘ 𝐵 )
isomushgr.e 𝐸 = ( Edg ‘ 𝐴 )
isomushgr.k 𝐾 = ( Edg ‘ 𝐵 )
isomuspgrlem2.g 𝐺 = ( 𝑥𝐸 ↦ ( 𝐹𝑥 ) )
isomuspgrlem2.a ( 𝜑𝐴 ∈ USPGraph )
isomuspgrlem2.f ( 𝜑𝐹 : 𝑉1-1-onto𝑊 )
isomuspgrlem2.i ( 𝜑 → ∀ 𝑎𝑉𝑏𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹𝑎 ) , ( 𝐹𝑏 ) } ∈ 𝐾 ) )
isomuspgrlem2.x ( 𝜑𝐹𝑋 )
Assertion isomuspgrlem2c ( 𝜑𝐺 : 𝐸1-1𝐾 )

### Proof

Step Hyp Ref Expression
1 isomushgr.v 𝑉 = ( Vtx ‘ 𝐴 )
2 isomushgr.w 𝑊 = ( Vtx ‘ 𝐵 )
3 isomushgr.e 𝐸 = ( Edg ‘ 𝐴 )
4 isomushgr.k 𝐾 = ( Edg ‘ 𝐵 )
5 isomuspgrlem2.g 𝐺 = ( 𝑥𝐸 ↦ ( 𝐹𝑥 ) )
6 isomuspgrlem2.a ( 𝜑𝐴 ∈ USPGraph )
7 isomuspgrlem2.f ( 𝜑𝐹 : 𝑉1-1-onto𝑊 )
8 isomuspgrlem2.i ( 𝜑 → ∀ 𝑎𝑉𝑏𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹𝑎 ) , ( 𝐹𝑏 ) } ∈ 𝐾 ) )
9 isomuspgrlem2.x ( 𝜑𝐹𝑋 )
10 1 2 3 4 5 6 7 8 isomuspgrlem2b ( 𝜑𝐺 : 𝐸𝐾 )
11 1 2 3 4 5 isomuspgrlem2a ( 𝐹𝑋 → ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) )
12 9 11 syl ( 𝜑 → ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) )
13 imaeq2 ( 𝑒 = 𝑐 → ( 𝐹𝑒 ) = ( 𝐹𝑐 ) )
14 fveq2 ( 𝑒 = 𝑐 → ( 𝐺𝑒 ) = ( 𝐺𝑐 ) )
15 13 14 eqeq12d ( 𝑒 = 𝑐 → ( ( 𝐹𝑒 ) = ( 𝐺𝑒 ) ↔ ( 𝐹𝑐 ) = ( 𝐺𝑐 ) ) )
16 15 rspcv ( 𝑐𝐸 → ( ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) → ( 𝐹𝑐 ) = ( 𝐺𝑐 ) ) )
17 16 ad2antrl ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) → ( ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) → ( 𝐹𝑐 ) = ( 𝐺𝑐 ) ) )
18 17 imp ( ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) ∧ ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) ) → ( 𝐹𝑐 ) = ( 𝐺𝑐 ) )
19 18 eqcomd ( ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) ∧ ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) ) → ( 𝐺𝑐 ) = ( 𝐹𝑐 ) )
20 imaeq2 ( 𝑒 = 𝑑 → ( 𝐹𝑒 ) = ( 𝐹𝑑 ) )
21 fveq2 ( 𝑒 = 𝑑 → ( 𝐺𝑒 ) = ( 𝐺𝑑 ) )
22 20 21 eqeq12d ( 𝑒 = 𝑑 → ( ( 𝐹𝑒 ) = ( 𝐺𝑒 ) ↔ ( 𝐹𝑑 ) = ( 𝐺𝑑 ) ) )
23 22 rspcv ( 𝑑𝐸 → ( ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) → ( 𝐹𝑑 ) = ( 𝐺𝑑 ) ) )
24 23 ad2antll ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) → ( ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) → ( 𝐹𝑑 ) = ( 𝐺𝑑 ) ) )
25 24 imp ( ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) ∧ ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) ) → ( 𝐹𝑑 ) = ( 𝐺𝑑 ) )
26 25 eqcomd ( ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) ∧ ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) ) → ( 𝐺𝑑 ) = ( 𝐹𝑑 ) )
27 19 26 eqeq12d ( ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) ∧ ∀ 𝑒𝐸 ( 𝐹𝑒 ) = ( 𝐺𝑒 ) ) → ( ( 𝐺𝑐 ) = ( 𝐺𝑑 ) ↔ ( 𝐹𝑐 ) = ( 𝐹𝑑 ) ) )
28 12 27 mpidan ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) → ( ( 𝐺𝑐 ) = ( 𝐺𝑑 ) ↔ ( 𝐹𝑐 ) = ( 𝐹𝑑 ) ) )
29 f1of1 ( 𝐹 : 𝑉1-1-onto𝑊𝐹 : 𝑉1-1𝑊 )
30 7 29 syl ( 𝜑𝐹 : 𝑉1-1𝑊 )
31 uspgrupgr ( 𝐴 ∈ USPGraph → 𝐴 ∈ UPGraph )
32 upgruhgr ( 𝐴 ∈ UPGraph → 𝐴 ∈ UHGraph )
33 3 eleq2i ( 𝑐𝐸𝑐 ∈ ( Edg ‘ 𝐴 ) )
34 edguhgr ( ( 𝐴 ∈ UHGraph ∧ 𝑐 ∈ ( Edg ‘ 𝐴 ) ) → 𝑐 ∈ 𝒫 ( Vtx ‘ 𝐴 ) )
35 elpwi ( 𝑐 ∈ 𝒫 ( Vtx ‘ 𝐴 ) → 𝑐 ⊆ ( Vtx ‘ 𝐴 ) )
36 35 1 sseqtrrdi ( 𝑐 ∈ 𝒫 ( Vtx ‘ 𝐴 ) → 𝑐𝑉 )
37 34 36 syl ( ( 𝐴 ∈ UHGraph ∧ 𝑐 ∈ ( Edg ‘ 𝐴 ) ) → 𝑐𝑉 )
38 37 ex ( 𝐴 ∈ UHGraph → ( 𝑐 ∈ ( Edg ‘ 𝐴 ) → 𝑐𝑉 ) )
39 33 38 syl5bi ( 𝐴 ∈ UHGraph → ( 𝑐𝐸𝑐𝑉 ) )
40 3 eleq2i ( 𝑑𝐸𝑑 ∈ ( Edg ‘ 𝐴 ) )
41 edguhgr ( ( 𝐴 ∈ UHGraph ∧ 𝑑 ∈ ( Edg ‘ 𝐴 ) ) → 𝑑 ∈ 𝒫 ( Vtx ‘ 𝐴 ) )
42 elpwi ( 𝑑 ∈ 𝒫 ( Vtx ‘ 𝐴 ) → 𝑑 ⊆ ( Vtx ‘ 𝐴 ) )
43 42 1 sseqtrrdi ( 𝑑 ∈ 𝒫 ( Vtx ‘ 𝐴 ) → 𝑑𝑉 )
44 41 43 syl ( ( 𝐴 ∈ UHGraph ∧ 𝑑 ∈ ( Edg ‘ 𝐴 ) ) → 𝑑𝑉 )
45 44 ex ( 𝐴 ∈ UHGraph → ( 𝑑 ∈ ( Edg ‘ 𝐴 ) → 𝑑𝑉 ) )
46 40 45 syl5bi ( 𝐴 ∈ UHGraph → ( 𝑑𝐸𝑑𝑉 ) )
47 39 46 anim12d ( 𝐴 ∈ UHGraph → ( ( 𝑐𝐸𝑑𝐸 ) → ( 𝑐𝑉𝑑𝑉 ) ) )
48 32 47 syl ( 𝐴 ∈ UPGraph → ( ( 𝑐𝐸𝑑𝐸 ) → ( 𝑐𝑉𝑑𝑉 ) ) )
49 6 31 48 3syl ( 𝜑 → ( ( 𝑐𝐸𝑑𝐸 ) → ( 𝑐𝑉𝑑𝑉 ) ) )
50 49 imp ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) → ( 𝑐𝑉𝑑𝑉 ) )
51 f1imaeq ( ( 𝐹 : 𝑉1-1𝑊 ∧ ( 𝑐𝑉𝑑𝑉 ) ) → ( ( 𝐹𝑐 ) = ( 𝐹𝑑 ) ↔ 𝑐 = 𝑑 ) )
52 30 50 51 syl2an2r ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) → ( ( 𝐹𝑐 ) = ( 𝐹𝑑 ) ↔ 𝑐 = 𝑑 ) )
53 52 biimpd ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) → ( ( 𝐹𝑐 ) = ( 𝐹𝑑 ) → 𝑐 = 𝑑 ) )
54 28 53 sylbid ( ( 𝜑 ∧ ( 𝑐𝐸𝑑𝐸 ) ) → ( ( 𝐺𝑐 ) = ( 𝐺𝑑 ) → 𝑐 = 𝑑 ) )
55 54 ralrimivva ( 𝜑 → ∀ 𝑐𝐸𝑑𝐸 ( ( 𝐺𝑐 ) = ( 𝐺𝑑 ) → 𝑐 = 𝑑 ) )
56 dff13 ( 𝐺 : 𝐸1-1𝐾 ↔ ( 𝐺 : 𝐸𝐾 ∧ ∀ 𝑐𝐸𝑑𝐸 ( ( 𝐺𝑐 ) = ( 𝐺𝑑 ) → 𝑐 = 𝑑 ) ) )
57 10 55 56 sylanbrc ( 𝜑𝐺 : 𝐸1-1𝐾 )