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 ‘ 𝑁 ) ) ∧ ∀ 𝑒 ∈ 𝐼 ( 𝐹 “ 𝑒 ) = ( 𝐻 ‘ 𝑒 ) ) )