Theorem isubgr3stgrlem2

Description: Lemma 2 for isubgr3stgr . (Contributed by AV, 16-Sep-2025)

	Ref	Expression
Hypotheses	isubgr3stgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isubgr3stgr.u	⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
	isubgr3stgr.c	⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
	isubgr3stgr.n	⊢ 𝑁 ∈ ℕ0
	isubgr3stgr.s	⊢ 𝑆 = ( StarGr ‘ 𝑁 )
	isubgr3stgr.w	⊢ 𝑊 = ( Vtx ‘ 𝑆 )
Assertion	isubgr3stgrlem2	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ∃ 𝑓 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) )

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	5 6	stgrorder	⊢ ( 𝑁 ∈ ℕ0 → ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) )
8	4 7	ax-mp	⊢ ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 )
9		oveq1	⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = ( ( 𝑁 + 1 ) − 1 ) )
10		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
11		pncan1	⊢ ( 𝑁 ∈ ℂ → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
12	10 11	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
13	4 12	mp1i	⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
14	9 13	eqtrd	⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = 𝑁 )
15	14	adantr	⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) → ( ( ♯ ‘ 𝑊 ) − 1 ) = 𝑁 )
16		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
17	4 16	ax-mp	⊢ ( 𝑁 + 1 ) ∈ ℕ0
18		eleq1	⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ↔ ( 𝑁 + 1 ) ∈ ℕ0 ) )
19	17 18	mpbiri	⊢ ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
20	19	adantr	⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
21	6	fvexi	⊢ 𝑊 ∈ V
22		hashclb	⊢ ( 𝑊 ∈ V → ( 𝑊 ∈ Fin ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) )
23	21 22	mp1i	⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) → ( 𝑊 ∈ Fin ↔ ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) )
24	20 23	mpbird	⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) → 𝑊 ∈ Fin )
25	5 6	stgrvtx0	⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ 𝑊 )
26	4 25	ax-mp	⊢ 0 ∈ 𝑊
27		hashdifsn	⊢ ( ( 𝑊 ∈ Fin ∧ 0 ∈ 𝑊 ) → ( ♯ ‘ ( 𝑊 ∖ { 0 } ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
28	24 26 27	sylancl	⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) → ( ♯ ‘ ( 𝑊 ∖ { 0 } ) ) = ( ( ♯ ‘ 𝑊 ) − 1 ) )
29		simpr3	⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) → ( ♯ ‘ 𝑈 ) = 𝑁 )
30	15 28 29	3eqtr4rd	⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) → ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( 𝑊 ∖ { 0 } ) ) )
31		eleq1	⊢ ( ( ♯ ‘ 𝑈 ) = 𝑁 → ( ( ♯ ‘ 𝑈 ) ∈ ℕ0 ↔ 𝑁 ∈ ℕ0 ) )
32	4 31	mpbiri	⊢ ( ( ♯ ‘ 𝑈 ) = 𝑁 → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
33	32	3ad2ant3	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ( ♯ ‘ 𝑈 ) ∈ ℕ0 )
34	2	ovexi	⊢ 𝑈 ∈ V
35		hashclb	⊢ ( 𝑈 ∈ V → ( 𝑈 ∈ Fin ↔ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ) )
36	34 35	mp1i	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ( 𝑈 ∈ Fin ↔ ( ♯ ‘ 𝑈 ) ∈ ℕ0 ) )
37	33 36	mpbird	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → 𝑈 ∈ Fin )
38		diffi	⊢ ( 𝑊 ∈ Fin → ( 𝑊 ∖ { 0 } ) ∈ Fin )
39	24 38	syl	⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) → ( 𝑊 ∖ { 0 } ) ∈ Fin )
40		hasheqf1o	⊢ ( ( 𝑈 ∈ Fin ∧ ( 𝑊 ∖ { 0 } ) ∈ Fin ) → ( ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( 𝑊 ∖ { 0 } ) ) ↔ ∃ 𝑓 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) ) )
41	37 39 40	syl2an2	⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) → ( ( ♯ ‘ 𝑈 ) = ( ♯ ‘ ( 𝑊 ∖ { 0 } ) ) ↔ ∃ 𝑓 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) ) )
42	30 41	mpbid	⊢ ( ( ( ♯ ‘ 𝑊 ) = ( 𝑁 + 1 ) ∧ ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ) → ∃ 𝑓 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) )
43	8 42	mpan	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ∃ 𝑓 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) )