Metamath Proof Explorer

Theorem isubgr3stgrlem3

Description: Lemma 3 for isubgr3stgr . (Contributed by AV, 17-Sep-2025)

Ref Expression
Hypotheses isubgr3stgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isubgr3stgr.u ⊢ 𝑈 = ( 𝐺 NeighbVtx 𝑋 )
isubgr3stgr.c ⊢ 𝐶 = ( 𝐺 ClNeighbVtx 𝑋 )
isubgr3stgr.n ⊢ 𝑁 ∈ ℕ0
isubgr3stgr.s ⊢ 𝑆 = ( StarGr ‘ 𝑁 )
isubgr3stgr.w ⊢ 𝑊 = ( Vtx ‘ 𝑆 )
Assertion isubgr3stgrlem3 ( ( 𝐺 ∈ 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 1 2 3 4 5 6 isubgr3stgrlem2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ∃ 𝑓 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) )
8 f1odm ⊢ ( 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) → dom 𝑓 = 𝑈 )
9 simpr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) ) → 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) )
10 simpl2 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) ) → 𝑋 ∈ 𝑉 )
11 c0ex ⊢ 0 ∈ V
12 11 a1i ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) ) → 0 ∈ V )
13 neldifsnd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) ) → ¬ 0 ∈ ( 𝑊 ∖ { 0 } ) )
14 df-nel ⊢ ( 0 ∉ ( 𝑊 ∖ { 0 } ) ↔ ¬ 0 ∈ ( 𝑊 ∖ { 0 } ) )
15 13 14 sylibr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) ) → 0 ∉ ( 𝑊 ∖ { 0 } ) )
16 eqid ⊢ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) = ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } )
17 1 2 3 16 isubgr3stgrlem1 ⊢ ( ( 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) ∧ 𝑋 ∈ 𝑉 ∧ ( 0 ∈ V ∧ 0 ∉ ( 𝑊 ∖ { 0 } ) ) ) → ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) )
18 9 10 12 15 17 syl112anc ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) ) → ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) )
19 18 ex ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ( 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) → ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ) )
20 f1of ⊢ ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) → ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 ⟶ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) )
21 20 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 ⟶ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) )
22 3 ovexi ⊢ 𝐶 ∈ V
23 22 a1i ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → 𝐶 ∈ V )
24 21 23 fexd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) ∈ V )
25 5 6 stgrvtx0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ 𝑊 )
26 4 25 mp1i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → 0 ∈ 𝑊 )
27 26 snssd ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → { 0 } ⊆ 𝑊 )
28 undifr ⊢ ( { 0 } ⊆ 𝑊 ↔ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) = 𝑊 )
29 27 28 sylib ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) = 𝑊 )
30 29 f1oeq3d ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ↔ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ 𝑊 ) )
31 30 biimpa ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ) → ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ 𝑊 )
32 31 3adant3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ 𝑊 )
33 simp12 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → 𝑋 ∈ 𝑉 )
34 11 a1i ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → 0 ∈ V )
35 nbgrnself2 ⊢ 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 )
36 df-nel ⊢ ( 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 ) ↔ ¬ 𝑋 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
37 2 eleq2i ⊢ ( 𝑋 ∈ 𝑈 ↔ 𝑋 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
38 36 37 xchbinxr ⊢ ( 𝑋 ∉ ( 𝐺 NeighbVtx 𝑋 ) ↔ ¬ 𝑋 ∈ 𝑈 )
39 35 38 mpbi ⊢ ¬ 𝑋 ∈ 𝑈
40 eleq2 ⊢ ( dom 𝑓 = 𝑈 → ( 𝑋 ∈ dom 𝑓 ↔ 𝑋 ∈ 𝑈 ) )
41 40 notbid ⊢ ( dom 𝑓 = 𝑈 → ( ¬ 𝑋 ∈ dom 𝑓 ↔ ¬ 𝑋 ∈ 𝑈 ) )
42 41 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → ( ¬ 𝑋 ∈ dom 𝑓 ↔ ¬ 𝑋 ∈ 𝑈 ) )
43 39 42 mpbiri ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → ¬ 𝑋 ∈ dom 𝑓 )
44 fsnunfv ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 0 ∈ V ∧ ¬ 𝑋 ∈ dom 𝑓 ) → ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) ‘ 𝑋 ) = 0 )
45 33 34 43 44 syl3anc ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) ‘ 𝑋 ) = 0 )
46 32 45 jca ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ 𝑊 ∧ ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) ‘ 𝑋 ) = 0 ) )
47 f1oeq1 ⊢ ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) → ( 𝑔 : 𝐶 –1-1-onto→ 𝑊 ↔ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ 𝑊 ) )
48 fveq1 ⊢ ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) → ( 𝑔 ‘ 𝑋 ) = ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) ‘ 𝑋 ) )
49 48 eqeq1d ⊢ ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) → ( ( 𝑔 ‘ 𝑋 ) = 0 ↔ ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) ‘ 𝑋 ) = 0 ) )
50 47 49 anbi12d ⊢ ( 𝑔 = ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) → ( ( 𝑔 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑔 ‘ 𝑋 ) = 0 ) ↔ ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ 𝑊 ∧ ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) ‘ 𝑋 ) = 0 ) ) )
51 24 46 50 spcedv ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) ∧ ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) ∧ dom 𝑓 = 𝑈 ) → ∃ 𝑔 ( 𝑔 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑔 ‘ 𝑋 ) = 0 ) )
52 51 3exp ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ( ( 𝑓 ∪ { ⟨ 𝑋 , 0 ⟩ } ) : 𝐶 –1-1-onto→ ( ( 𝑊 ∖ { 0 } ) ∪ { 0 } ) → ( dom 𝑓 = 𝑈 → ∃ 𝑔 ( 𝑔 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑔 ‘ 𝑋 ) = 0 ) ) ) )
53 19 52 syld ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ( 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) → ( dom 𝑓 = 𝑈 → ∃ 𝑔 ( 𝑔 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑔 ‘ 𝑋 ) = 0 ) ) ) )
54 8 53 mpdi ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ( 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) → ∃ 𝑔 ( 𝑔 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑔 ‘ 𝑋 ) = 0 ) ) )
55 54 exlimdv ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ( ∃ 𝑓 𝑓 : 𝑈 –1-1-onto→ ( 𝑊 ∖ { 0 } ) → ∃ 𝑔 ( 𝑔 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑔 ‘ 𝑋 ) = 0 ) ) )
56 7 55 mpd ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ ( ♯ ‘ 𝑈 ) = 𝑁 ) → ∃ 𝑔 ( 𝑔 : 𝐶 –1-1-onto→ 𝑊 ∧ ( 𝑔 ‘ 𝑋 ) = 0 ) )