Metamath Proof Explorer


Theorem isubgr3stgrlem9

Description: Lemma 9 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 isubgr3stgrlem9 ( ( ( ( 𝐺 ∈ 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 1 2 3 4 5 6 7 8 9 isubgr3stgrlem8 ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → 𝐻 : 𝐼1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) )
11 f1of ( 𝐹 : 𝐶1-1-onto𝑊𝐹 : 𝐶𝑊 )
12 11 ad2antrl ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → 𝐹 : 𝐶𝑊 )
13 1 2 3 4 5 6 7 8 9 isubgr3stgrlem5 ( ( 𝐹 : 𝐶𝑊𝑒𝐼 ) → ( 𝐻𝑒 ) = ( 𝐹𝑒 ) )
14 13 eqcomd ( ( 𝐹 : 𝐶𝑊𝑒𝐼 ) → ( 𝐹𝑒 ) = ( 𝐻𝑒 ) )
15 12 14 sylan ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) ∧ 𝑒𝐼 ) → ( 𝐹𝑒 ) = ( 𝐻𝑒 ) )
16 15 ralrimiva ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → ∀ 𝑒𝐼 ( 𝐹𝑒 ) = ( 𝐻𝑒 ) )
17 10 16 jca ( ( ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉 ) ∧ ( ( ♯ ‘ 𝑈 ) = 𝑁 ∧ ∀ 𝑥𝑈𝑦𝑈 { 𝑥 , 𝑦 } ∉ 𝐸 ) ) ∧ ( 𝐹 : 𝐶1-1-onto𝑊 ∧ ( 𝐹𝑋 ) = 0 ) ) → ( 𝐻 : 𝐼1-1-onto→ ( Edg ‘ ( StarGr ‘ 𝑁 ) ) ∧ ∀ 𝑒𝐼 ( 𝐹𝑒 ) = ( 𝐻𝑒 ) ) )