Metamath Proof Explorer


Theorem isubgr3stgrlem8

Description: Lemma 8 for isubgr3stgr . (Contributed by AV, 29-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v 𝑉 = ( Vtx ‘ 𝐺 )
isubgr3stgr.u 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
isubgr3stgr.c 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
isubgr3stgr.n 𝑁 ∈ ℕ0
isubgr3stgr.s 𝑆 = ( StarGr ‘ 𝑁 )
isubgr3stgr.w 𝑊 = ( Vtx ‘ 𝑆 )
isubgr3stgr.e 𝐸 = ( Edg ‘ 𝐺 )
isubgr3stgr.i 𝐼 = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) )
isubgr3stgr.h 𝐻 = ( 𝑖𝐼 ↦ ( 𝐹𝑖 ) )
Assertion isubgr3stgrlem8 ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → 𝐻 : 𝐼1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 isubgr3stgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgr3stgr.u 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
3 isubgr3stgr.c 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
4 isubgr3stgr.n 𝑁 ∈ ℕ0
5 isubgr3stgr.s 𝑆 = ( StarGr ‘ 𝑁 )
6 isubgr3stgr.w 𝑊 = ( Vtx ‘ 𝑆 )
7 isubgr3stgr.e 𝐸 = ( Edg ‘ 𝐺 )
8 isubgr3stgr.i 𝐼 = ( Edg ‘ ( 𝐺 ISubGr 𝐶 ) )
9 isubgr3stgr.h 𝐻 = ( 𝑖𝐼 ↦ ( 𝐹𝑖 ) )
10 imaeq2 ( 𝑖 = 𝑘 → ( 𝐹𝑖 ) = ( 𝐹𝑘 ) )
11 10 cbvmptv ( 𝑖𝐼 ↦ ( 𝐹𝑖 ) ) = ( 𝑘𝐼 ↦ ( 𝐹𝑘 ) )
12 9 11 eqtri 𝐻 = ( 𝑘𝐼 ↦ ( 𝐹𝑘 ) )
13 f1of ( 𝐹 : 𝐶1-1-onto𝑊𝐹 : 𝐶𝑊 )
14 13 ad2antrl ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → 𝐹 : 𝐶𝑊 )
15 1 2 3 4 5 6 7 8 9 isubgr3stgrlem5 ( ( 𝐹 : 𝐶𝑊𝑘𝐼 ) → ( 𝐻𝑘 ) = ( 𝐹𝑘 ) )
16 14 15 sylan ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ 𝑘𝐼 ) → ( 𝐻𝑘 ) = ( 𝐹𝑘 ) )
17 1 2 3 4 5 6 7 8 9 isubgr3stgrlem6 ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → 𝐻 : 𝐼 ⟶ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )
18 17 ffvelcdmda ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ 𝑘𝐼 ) → ( 𝐻𝑘 ) ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )
19 16 18 eqeltrrd ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ 𝑘𝐼 ) → ( 𝐹𝑘 ) ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )
20 1 2 3 4 5 6 7 8 9 isubgr3stgrlem7 ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( 𝐹𝑗 ) ∈ 𝐼 )
21 20 ad4ant134 ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( 𝐹𝑗 ) ∈ 𝐼 )
22 f1ofo ( 𝐹 : 𝐶1-1-onto𝑊𝐹 : 𝐶onto𝑊 )
23 22 ad2antrl ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → 𝐹 : 𝐶onto𝑊 )
24 stgrusgra ( 𝑁 ∈ ℕ0 → ( StarGr ‘ 𝑁 ) ∈ USGraph )
25 4 24 mp1i ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → ( StarGr ‘ 𝑁 ) ∈ USGraph )
26 simpr ( ( 𝑘𝐼𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )
27 5 fveq2i ( Vtx ‘ 𝑆 ) = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
28 6 27 eqtri 𝑊 = ( Vtx ‘ ( StarGr ‘ 𝑁 ) )
29 eqid ( Edg ‘ ( StarGr ‘ 𝑁 ) ) = ( Edg ‘ ( StarGr ‘ 𝑁 ) )
30 28 29 edgssv2 ( ( ( StarGr ‘ 𝑁 ) ∈ USGraph ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → ( 𝑗𝑊 ∧ ( ♯ ‘ 𝑗 ) = 2 ) )
31 30 simpld ( ( ( StarGr ‘ 𝑁 ) ∈ USGraph ∧ 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) → 𝑗𝑊 )
32 25 26 31 syl2an ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ ( 𝑘𝐼𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → 𝑗𝑊 )
33 foimacnv ( ( 𝐹 : 𝐶onto𝑊𝑗𝑊 ) → ( 𝐹 “ ( 𝐹𝑗 ) ) = 𝑗 )
34 23 32 33 syl2an2r ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ ( 𝑘𝐼𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → ( 𝐹 “ ( 𝐹𝑗 ) ) = 𝑗 )
35 imaeq2 ( 𝑘 = ( 𝐹𝑗 ) → ( 𝐹𝑘 ) = ( 𝐹 “ ( 𝐹𝑗 ) ) )
36 35 eqcomd ( 𝑘 = ( 𝐹𝑗 ) → ( 𝐹 “ ( 𝐹𝑗 ) ) = ( 𝐹𝑘 ) )
37 34 36 sylan9req ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ ( 𝑘𝐼𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) ∧ 𝑘 = ( 𝐹𝑗 ) ) → 𝑗 = ( 𝐹𝑘 ) )
38 imaeq2 ( 𝑗 = ( 𝐹𝑘 ) → ( 𝐹𝑗 ) = ( 𝐹 “ ( 𝐹𝑘 ) ) )
39 f1of1 ( 𝐹 : 𝐶1-1-onto𝑊𝐹 : 𝐶1-1𝑊 )
40 39 ad2antrl ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → 𝐹 : 𝐶1-1𝑊 )
41 usgruhgr ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
42 41 ad2antrr ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) → 𝐺 ∈ UHGraph )
43 1 clnbgrssvtx ( 𝐺 ClNeighbVtx 𝑋 ) ⊆ 𝑉
44 3 43 eqsstri 𝐶𝑉
45 44 a1i ( ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) → 𝐶𝑉 )
46 eqid ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
47 eqid ( 𝐺 ISubGr 𝐶 ) = ( 𝐺 ISubGr 𝐶 )
48 1 46 47 8 isubgredg ( ( 𝐺 ∈ UHGraph ∧ 𝐶𝑉 ) → ( 𝑘𝐼 ↔ ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘𝐶 ) ) )
49 42 45 48 syl2an ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → ( 𝑘𝐼 ↔ ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘𝐶 ) ) )
50 simpr ( ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘𝐶 ) → 𝑘𝐶 )
51 50 a1d ( ( 𝑘 ∈ ( Edg ‘ 𝐺 ) ∧ 𝑘𝐶 ) → ( 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) → 𝑘𝐶 ) )
52 49 51 biimtrdi ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → ( 𝑘𝐼 → ( 𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) → 𝑘𝐶 ) ) )
53 52 imp32 ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ ( 𝑘𝐼𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → 𝑘𝐶 )
54 f1imacnv ( ( 𝐹 : 𝐶1-1𝑊𝑘𝐶 ) → ( 𝐹 “ ( 𝐹𝑘 ) ) = 𝑘 )
55 40 53 54 syl2an2r ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ ( 𝑘𝐼𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → ( 𝐹 “ ( 𝐹𝑘 ) ) = 𝑘 )
56 38 55 sylan9eqr ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ ( 𝑘𝐼𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) ∧ 𝑗 = ( 𝐹𝑘 ) ) → ( 𝐹𝑗 ) = 𝑘 )
57 56 eqcomd ( ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ ( 𝑘𝐼𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) ∧ 𝑗 = ( 𝐹𝑘 ) ) → 𝑘 = ( 𝐹𝑗 ) )
58 37 57 impbida ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ ( 𝑘𝐼𝑗 ∈ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ) ) → ( 𝑘 = ( 𝐹𝑗 ) ↔ 𝑗 = ( 𝐹𝑘 ) ) )
59 12 19 21 58 f1o2d ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → 𝐻 : 𝐼1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )