Metamath Proof Explorer

Theorem isomuspgrlem2d

Description: Lemma 4 for isomuspgrlem2 . (Contributed by AV, 1-Dec-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 ⊢ ( 𝜑 → 𝐹 ∈ 𝑋 )
isomuspgrlem2.b ⊢ ( 𝜑 → 𝐵 ∈ USPGraph )
Assertion isomuspgrlem2d ( 𝜑 → 𝐺 : 𝐸 –onto→ 𝐾 )

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 isomuspgrlem2.b ⊢ ( 𝜑 → 𝐵 ∈ USPGraph )
11 1 2 3 4 5 6 7 8 isomuspgrlem2b ⊢ ( 𝜑 → 𝐺 : 𝐸 ⟶ 𝐾 )
12 uspgrupgr ⊢ ( 𝐵 ∈ USPGraph → 𝐵 ∈ UPGraph )
13 10 12 syl ⊢ ( 𝜑 → 𝐵 ∈ UPGraph )
14 2 4 upgredg ⊢ ( ( 𝐵 ∈ UPGraph ∧ 𝑦 ∈ 𝐾 ) → ∃ 𝑐 ∈ 𝑊 ∃ 𝑑 ∈ 𝑊 𝑦 = { 𝑐 , 𝑑 } )
15 13 14 sylan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ∃ 𝑐 ∈ 𝑊 ∃ 𝑑 ∈ 𝑊 𝑦 = { 𝑐 , 𝑑 } )
16 eleq1 ⊢ ( 𝑦 = { 𝑐 , 𝑑 } → ( 𝑦 ∈ 𝐾 ↔ { 𝑐 , 𝑑 } ∈ 𝐾 ) )
17 16 anbi2d ⊢ ( 𝑦 = { 𝑐 , 𝑑 } → ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ↔ ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ) )
18 f1ofo ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 –onto→ 𝑊 )
19 7 18 syl ⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝑊 )
20 foelrn ⊢ ( ( 𝐹 : 𝑉 –onto→ 𝑊 ∧ 𝑐 ∈ 𝑊 ) → ∃ 𝑚 ∈ 𝑉 𝑐 = ( 𝐹 ‘ 𝑚 ) )
21 19 20 sylan ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑊 ) → ∃ 𝑚 ∈ 𝑉 𝑐 = ( 𝐹 ‘ 𝑚 ) )
22 21 ex ⊢ ( 𝜑 → ( 𝑐 ∈ 𝑊 → ∃ 𝑚 ∈ 𝑉 𝑐 = ( 𝐹 ‘ 𝑚 ) ) )
23 foelrn ⊢ ( ( 𝐹 : 𝑉 –onto→ 𝑊 ∧ 𝑑 ∈ 𝑊 ) → ∃ 𝑛 ∈ 𝑉 𝑑 = ( 𝐹 ‘ 𝑛 ) )
24 19 23 sylan ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝑊 ) → ∃ 𝑛 ∈ 𝑉 𝑑 = ( 𝐹 ‘ 𝑛 ) )
25 24 ex ⊢ ( 𝜑 → ( 𝑑 ∈ 𝑊 → ∃ 𝑛 ∈ 𝑉 𝑑 = ( 𝐹 ‘ 𝑛 ) ) )
26 22 25 anim12d ⊢ ( 𝜑 → ( ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) → ( ∃ 𝑚 ∈ 𝑉 𝑐 = ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ 𝑉 𝑑 = ( 𝐹 ‘ 𝑛 ) ) ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) → ( ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) → ( ∃ 𝑚 ∈ 𝑉 𝑐 = ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ 𝑉 𝑑 = ( 𝐹 ‘ 𝑛 ) ) ) )
28 27 imp ⊢ ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → ( ∃ 𝑚 ∈ 𝑉 𝑐 = ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ 𝑉 𝑑 = ( 𝐹 ‘ 𝑛 ) ) )
29 preq12 ⊢ ( ( 𝑐 = ( 𝐹 ‘ 𝑚 ) ∧ 𝑑 = ( 𝐹 ‘ 𝑛 ) ) → { 𝑐 , 𝑑 } = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
30 29 ancoms ⊢ ( ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) → { 𝑐 , 𝑑 } = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
31 30 eleq1d ⊢ ( ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) → ( { 𝑐 , 𝑑 } ∈ 𝐾 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐾 ) )
32 preq1 ⊢ ( 𝑎 = 𝑚 → { 𝑎 , 𝑏 } = { 𝑚 , 𝑏 } )
33 32 eleq1d ⊢ ( 𝑎 = 𝑚 → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { 𝑚 , 𝑏 } ∈ 𝐸 ) )
34 fveq2 ⊢ ( 𝑎 = 𝑚 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑚 ) )
35 34 preq1d ⊢ ( 𝑎 = 𝑚 → { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑏 ) } )
36 35 eleq1d ⊢ ( 𝑎 = 𝑚 → ( { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) )
37 33 36 bibi12d ⊢ ( 𝑎 = 𝑚 → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) ↔ ( { 𝑚 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) ) )
38 preq2 ⊢ ( 𝑏 = 𝑛 → { 𝑚 , 𝑏 } = { 𝑚 , 𝑛 } )
39 38 eleq1d ⊢ ( 𝑏 = 𝑛 → ( { 𝑚 , 𝑏 } ∈ 𝐸 ↔ { 𝑚 , 𝑛 } ∈ 𝐸 ) )
40 fveq2 ⊢ ( 𝑏 = 𝑛 → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑛 ) )
41 40 preq2d ⊢ ( 𝑏 = 𝑛 → { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑏 ) } = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
42 41 eleq1d ⊢ ( 𝑏 = 𝑛 → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐾 ) )
43 39 42 bibi12d ⊢ ( 𝑏 = 𝑛 → ( ( { 𝑚 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) ↔ ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐾 ) ) )
44 37 43 rspc2va ⊢ ( ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) ) → ( { 𝑚 , 𝑛 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐾 ) )
45 44 bicomd ⊢ ( ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐾 ↔ { 𝑚 , 𝑛 } ∈ 𝐸 ) )
46 45 ancoms ⊢ ( ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐾 ↔ { 𝑚 , 𝑛 } ∈ 𝐸 ) )
47 46 biimpd ⊢ ( ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐾 → { 𝑚 , 𝑛 } ∈ 𝐸 ) )
48 47 ex ⊢ ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝐹 ‘ 𝑎 ) , ( 𝐹 ‘ 𝑏 ) } ∈ 𝐾 ) → ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐾 → { 𝑚 , 𝑛 } ∈ 𝐸 ) ) )
49 8 48 syl ⊢ ( 𝜑 → ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐾 → { 𝑚 , 𝑛 } ∈ 𝐸 ) ) )
50 49 com13 ⊢ ( { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ∈ 𝐾 → ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( 𝜑 → { 𝑚 , 𝑛 } ∈ 𝐸 ) ) )
51 31 50 syl6bi ⊢ ( ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) → ( { 𝑐 , 𝑑 } ∈ 𝐾 → ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( 𝜑 → { 𝑚 , 𝑛 } ∈ 𝐸 ) ) ) )
52 51 com14 ⊢ ( 𝜑 → ( { 𝑐 , 𝑑 } ∈ 𝐾 → ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) → { 𝑚 , 𝑛 } ∈ 𝐸 ) ) ) )
53 52 imp ⊢ ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) → ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) → { 𝑚 , 𝑛 } ∈ 𝐸 ) ) )
54 53 adantr ⊢ ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) → { 𝑚 , 𝑛 } ∈ 𝐸 ) ) )
55 54 imp31 ⊢ ( ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) ) → { 𝑚 , 𝑛 } ∈ 𝐸 )
56 imaeq2 ⊢ ( 𝑒 = { 𝑚 , 𝑛 } → ( 𝐹 “ 𝑒 ) = ( 𝐹 “ { 𝑚 , 𝑛 } ) )
57 f1ofn ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 Fn 𝑉 )
58 7 57 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑉 )
59 58 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → 𝐹 Fn 𝑉 )
60 simprl ⊢ ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑚 ∈ 𝑉 )
61 simpr ⊢ ( ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → 𝑛 ∈ 𝑉 )
62 61 adantl ⊢ ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → 𝑛 ∈ 𝑉 )
63 59 60 62 3jca ⊢ ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( 𝐹 Fn 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) )
64 63 adantr ⊢ ( ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝐹 Fn 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) )
65 fnimapr ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) → ( 𝐹 “ { 𝑚 , 𝑛 } ) = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
66 64 65 syl ⊢ ( ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) ) → ( 𝐹 “ { 𝑚 , 𝑛 } ) = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
67 56 66 sylan9eqr ⊢ ( ( ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) ) ∧ 𝑒 = { 𝑚 , 𝑛 } ) → ( 𝐹 “ 𝑒 ) = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
68 67 eqeq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) ) ∧ 𝑒 = { 𝑚 , 𝑛 } ) → ( { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ↔ { 𝑐 , 𝑑 } = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } ) )
69 30 adantl ⊢ ( ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) ) → { 𝑐 , 𝑑 } = { ( 𝐹 ‘ 𝑚 ) , ( 𝐹 ‘ 𝑛 ) } )
70 55 68 69 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) ∧ ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) )
71 70 ex ⊢ ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ ( 𝑚 ∈ 𝑉 ∧ 𝑛 ∈ 𝑉 ) ) → ( ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) )
72 71 anassrs ⊢ ( ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑛 ∈ 𝑉 ) → ( ( 𝑑 = ( 𝐹 ‘ 𝑛 ) ∧ 𝑐 = ( 𝐹 ‘ 𝑚 ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) )
73 72 expd ⊢ ( ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ 𝑛 ∈ 𝑉 ) → ( 𝑑 = ( 𝐹 ‘ 𝑛 ) → ( 𝑐 = ( 𝐹 ‘ 𝑚 ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) ) )
74 73 rexlimdva ⊢ ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) → ( ∃ 𝑛 ∈ 𝑉 𝑑 = ( 𝐹 ‘ 𝑛 ) → ( 𝑐 = ( 𝐹 ‘ 𝑚 ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) ) )
75 74 com23 ⊢ ( ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑚 ∈ 𝑉 ) → ( 𝑐 = ( 𝐹 ‘ 𝑚 ) → ( ∃ 𝑛 ∈ 𝑉 𝑑 = ( 𝐹 ‘ 𝑛 ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) ) )
76 75 rexlimdva ⊢ ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → ( ∃ 𝑚 ∈ 𝑉 𝑐 = ( 𝐹 ‘ 𝑚 ) → ( ∃ 𝑛 ∈ 𝑉 𝑑 = ( 𝐹 ‘ 𝑛 ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) ) )
77 76 impd ⊢ ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → ( ( ∃ 𝑚 ∈ 𝑉 𝑐 = ( 𝐹 ‘ 𝑚 ) ∧ ∃ 𝑛 ∈ 𝑉 𝑑 = ( 𝐹 ‘ 𝑛 ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) )
78 28 77 mpd ⊢ ( ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) )
79 78 ex ⊢ ( ( 𝜑 ∧ { 𝑐 , 𝑑 } ∈ 𝐾 ) → ( ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) )
80 17 79 syl6bi ⊢ ( 𝑦 = { 𝑐 , 𝑑 } → ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) ) )
81 80 impd ⊢ ( 𝑦 = { 𝑐 , 𝑑 } → ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) )
82 81 impcom ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑦 = { 𝑐 , 𝑑 } ) → ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) )
83 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑦 = { 𝑐 , 𝑑 } ) → 𝑦 = { 𝑐 , 𝑑 } )
84 83 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑦 = { 𝑐 , 𝑑 } ) ∧ 𝑒 ∈ 𝐸 ) → 𝑦 = { 𝑐 , 𝑑 } )
85 9 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑦 = { 𝑐 , 𝑑 } ) ∧ 𝑒 ∈ 𝐸 ) → 𝐹 ∈ 𝑋 )
86 1 2 3 4 5 isomuspgrlem2a ⊢ ( 𝐹 ∈ 𝑋 → ∀ 𝑦 ∈ 𝐸 ( 𝐹 “ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
87 85 86 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑦 = { 𝑐 , 𝑑 } ) ∧ 𝑒 ∈ 𝐸 ) → ∀ 𝑦 ∈ 𝐸 ( 𝐹 “ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
88 imaeq2 ⊢ ( 𝑦 = 𝑒 → ( 𝐹 “ 𝑦 ) = ( 𝐹 “ 𝑒 ) )
89 fveq2 ⊢ ( 𝑦 = 𝑒 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑒 ) )
90 88 89 eqeq12d ⊢ ( 𝑦 = 𝑒 → ( ( 𝐹 “ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ) )
91 90 rspcv ⊢ ( 𝑒 ∈ 𝐸 → ( ∀ 𝑦 ∈ 𝐸 ( 𝐹 “ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) ) )
92 eqcom ⊢ ( ( 𝐺 ‘ 𝑒 ) = ( 𝐹 “ 𝑒 ) ↔ ( 𝐹 “ 𝑒 ) = ( 𝐺 ‘ 𝑒 ) )
93 91 92 syl6ibr ⊢ ( 𝑒 ∈ 𝐸 → ( ∀ 𝑦 ∈ 𝐸 ( 𝐹 “ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝐺 ‘ 𝑒 ) = ( 𝐹 “ 𝑒 ) ) )
94 93 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑦 = { 𝑐 , 𝑑 } ) ∧ 𝑒 ∈ 𝐸 ) → ( ∀ 𝑦 ∈ 𝐸 ( 𝐹 “ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝐺 ‘ 𝑒 ) = ( 𝐹 “ 𝑒 ) ) )
95 87 94 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑦 = { 𝑐 , 𝑑 } ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝐺 ‘ 𝑒 ) = ( 𝐹 “ 𝑒 ) )
96 84 95 eqeq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑦 = { 𝑐 , 𝑑 } ) ∧ 𝑒 ∈ 𝐸 ) → ( 𝑦 = ( 𝐺 ‘ 𝑒 ) ↔ { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) )
97 96 rexbidva ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑦 = { 𝑐 , 𝑑 } ) → ( ∃ 𝑒 ∈ 𝐸 𝑦 = ( 𝐺 ‘ 𝑒 ) ↔ ∃ 𝑒 ∈ 𝐸 { 𝑐 , 𝑑 } = ( 𝐹 “ 𝑒 ) ) )
98 82 97 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) ∧ 𝑦 = { 𝑐 , 𝑑 } ) → ∃ 𝑒 ∈ 𝐸 𝑦 = ( 𝐺 ‘ 𝑒 ) )
99 98 ex ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) ∧ ( 𝑐 ∈ 𝑊 ∧ 𝑑 ∈ 𝑊 ) ) → ( 𝑦 = { 𝑐 , 𝑑 } → ∃ 𝑒 ∈ 𝐸 𝑦 = ( 𝐺 ‘ 𝑒 ) ) )
100 99 rexlimdvva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ( ∃ 𝑐 ∈ 𝑊 ∃ 𝑑 ∈ 𝑊 𝑦 = { 𝑐 , 𝑑 } → ∃ 𝑒 ∈ 𝐸 𝑦 = ( 𝐺 ‘ 𝑒 ) ) )
101 15 100 mpd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐾 ) → ∃ 𝑒 ∈ 𝐸 𝑦 = ( 𝐺 ‘ 𝑒 ) )
102 101 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐾 ∃ 𝑒 ∈ 𝐸 𝑦 = ( 𝐺 ‘ 𝑒 ) )
103 dffo3 ⊢ ( 𝐺 : 𝐸 –onto→ 𝐾 ↔ ( 𝐺 : 𝐸 ⟶ 𝐾 ∧ ∀ 𝑦 ∈ 𝐾 ∃ 𝑒 ∈ 𝐸 𝑦 = ( 𝐺 ‘ 𝑒 ) ) )
104 11 102 103 sylanbrc ⊢ ( 𝜑 → 𝐺 : 𝐸 –onto→ 𝐾 )