Metamath Proof Explorer

Theorem isomuspgrlem2b

Description: Lemma 2 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 ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) )
Assertion isomuspgrlem2b ( 𝜑 → 𝐺 : 𝐸 ⟶ 𝐾 )

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 uspgrupgr ⊢ ( 𝐴 ∈ USPGraph → 𝐴 ∈ UPGraph )
10 6 9 syl ⊢ ( 𝜑 → 𝐴 ∈ UPGraph )
11 1 3 upgredg ⊢ ( ( 𝐴 ∈ UPGraph ∧ 𝑥 ∈ 𝐸 ) → ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 𝑥 = { 𝑐 , 𝑑 } )
12 10 11 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) → ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 𝑥 = { 𝑐 , 𝑑 } )
13 preq12 ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → { 𝑎 , 𝑏 } = { 𝑐 , 𝑑 } )
14 13 eleq1d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { 𝑐 , 𝑑 } ∈ 𝐸 ) )
15 fveq2 ⊢ ( 𝑎 = 𝑐 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑐 ) )
16 15 adantr ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑐 ) )
17 fveq2 ⊢ ( 𝑏 = 𝑑 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑑 ) )
18 17 adantl ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑑 ) )
19 16 18 preq12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } = { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } )
20 19 eleq1d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ↔ { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) )
21 14 20 bibi12d ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) ↔ ( { 𝑐 , 𝑑 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) ) )
22 21 rspc2gv ⊢ ( ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) → ( { 𝑐 , 𝑑 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) ) )
23 8 22 syl5com ⊢ ( 𝜑 → ( ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) → ( { 𝑐 , 𝑑 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) → ( ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) → ( { 𝑐 , 𝑑 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) ) )
25 24 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( { 𝑐 , 𝑑 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) )
26 bicom ⊢ ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) ↔ ( { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ↔ { 𝑐 , 𝑑 } ∈ 𝐸 ) )
27 bianir ⊢ ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ ( { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ↔ { 𝑐 , 𝑑 } ∈ 𝐸 ) ) → { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 )
28 27 ex ⊢ ( { 𝑐 , 𝑑 } ∈ 𝐸 → ( ( { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ↔ { 𝑐 , 𝑑 } ∈ 𝐸 ) → { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) )
29 26 28 syl5bi ⊢ ( { 𝑐 , 𝑑 } ∈ 𝐸 → ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) → { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) )
30 f1ofn ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 Fn 𝑉 )
31 7 30 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑉 )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) → 𝐹 Fn 𝑉 )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → 𝐹 Fn 𝑉 )
34 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → 𝑐 ∈ 𝑉 )
35 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → 𝑑 ∈ 𝑉 )
36 33 34 35 3jca ⊢ ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) )
37 36 adantl ⊢ ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( 𝐹 Fn 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) )
38 fnimapr ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) → ( 𝐹 “ { 𝑐 , 𝑑 } ) = { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } )
39 37 38 syl ⊢ ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( 𝐹 “ { 𝑐 , 𝑑 } ) = { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } )
40 39 eqcomd ⊢ ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } = ( 𝐹 “ { 𝑐 , 𝑑 } ) )
41 40 eleq1d ⊢ ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ↔ ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) )
42 41 biimpd ⊢ ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ∧ ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) ) → ( { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 → ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) )
43 42 ex ⊢ ( { 𝑐 , 𝑑 } ∈ 𝐸 → ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 → ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) ) )
44 43 com23 ⊢ ( { 𝑐 , 𝑑 } ∈ 𝐸 → ( { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 → ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) ) )
45 29 44 syld ⊢ ( { 𝑐 , 𝑑 } ∈ 𝐸 → ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) → ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) ) )
46 45 com13 ⊢ ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( ( { 𝑐 , 𝑑 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑐 ) , ( 𝐹 ‘ 𝑑 ) } ∈ 𝐾 ) → ( { 𝑐 , 𝑑 } ∈ 𝐸 → ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) ) )
47 25 46 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( { 𝑐 , 𝑑 } ∈ 𝐸 → ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) )
48 eleq1 ⊢ ( 𝑥 = { 𝑐 , 𝑑 } → ( 𝑥 ∈ 𝐸 ↔ { 𝑐 , 𝑑 } ∈ 𝐸 ) )
49 imaeq2 ⊢ ( 𝑥 = { 𝑐 , 𝑑 } → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ { 𝑐 , 𝑑 } ) )
50 49 eleq1d ⊢ ( 𝑥 = { 𝑐 , 𝑑 } → ( ( 𝐹 “ 𝑥 ) ∈ 𝐾 ↔ ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) )
51 48 50 imbi12d ⊢ ( 𝑥 = { 𝑐 , 𝑑 } → ( ( 𝑥 ∈ 𝐸 → ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) ↔ ( { 𝑐 , 𝑑 } ∈ 𝐸 → ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) ) )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) → ( ( 𝑥 ∈ 𝐸 → ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) ↔ ( { 𝑐 , 𝑑 } ∈ 𝐸 → ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) ) )
53 52 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝐸 → ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) ↔ ( { 𝑐 , 𝑑 } ∈ 𝐸 → ( 𝐹 “ { 𝑐 , 𝑑 } ) ∈ 𝐾 ) ) )
54 47 53 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 = { 𝑐 , 𝑑 } ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝐸 → ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) )
55 54 exp31 ⊢ ( 𝜑 → ( 𝑥 = { 𝑐 , 𝑑 } → ( ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐸 → ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) ) ) )
56 55 com24 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐸 → ( ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) → ( 𝑥 = { 𝑐 , 𝑑 } → ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) ) ) )
57 56 imp31 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) ∧ ( 𝑐 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉 ) ) → ( 𝑥 = { 𝑐 , 𝑑 } → ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) )
58 57 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) → ( ∃ 𝑐 ∈ 𝑉 ∃ 𝑑 ∈ 𝑉 𝑥 = { 𝑐 , 𝑑 } → ( 𝐹 “ 𝑥 ) ∈ 𝐾 ) )
59 12 58 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐸 ) → ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
60 59 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐸 ( 𝐹 “ 𝑥 ) ∈ 𝐾 )
61 5 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐸 ( 𝐹 “ 𝑥 ) ∈ 𝐾 ↔ 𝐺 : 𝐸 ⟶ 𝐾 )
62 60 61 sylib ⊢ ( 𝜑 → 𝐺 : 𝐸 ⟶ 𝐾 )