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 ) )