Metamath Proof Explorer

Theorem isubgr3stgrlem2

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

Ref Expression
Hypotheses isubgr3stgr.v ⊢ V = Vtx ⁡ G
isubgr3stgr.u ⊢ U = G NeighbVtx X
isubgr3stgr.c ⊢ C = G ClNeighbVtx X
isubgr3stgr.n ⊢ N ∈ ℕ 0
isubgr3stgr.s No typesetting found for |- S = ( StarGr ` N ) with typecode |-
isubgr3stgr.w ⊢ W = Vtx ⁡ S
Assertion isubgr3stgrlem2 ⊢ G ∈ USGraph ∧ X ∈ V ∧ U = N → ∃ f f : U ⟶ 1-1 onto W ∖ 0

Proof

Step Hyp Ref Expression
1 isubgr3stgr.v ⊢ V = Vtx ⁡ G
2 isubgr3stgr.u ⊢ U = G NeighbVtx X
3 isubgr3stgr.c ⊢ C = G ClNeighbVtx X
4 isubgr3stgr.n ⊢ N ∈ ℕ 0
5 isubgr3stgr.s Could not format S = ( StarGr ` N ) : No typesetting found for |- S = ( StarGr ` N ) with typecode |-
6 isubgr3stgr.w ⊢ W = Vtx ⁡ S
7 5 6 stgrorder ⊢ N ∈ ℕ 0 → W = N + 1
8 4 7 ax-mp ⊢ W = N + 1
9 oveq1 ⊢ W = N + 1 → W − 1 = N + 1 - 1
10 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
11 pncan1 ⊢ N ∈ ℂ → N + 1 - 1 = N
12 10 11 syl ⊢ N ∈ ℕ 0 → N + 1 - 1 = N
13 4 12 mp1i ⊢ W = N + 1 → N + 1 - 1 = N
14 9 13 eqtrd ⊢ W = N + 1 → W − 1 = N
15 14 adantr ⊢ W = N + 1 ∧ G ∈ USGraph ∧ X ∈ V ∧ U = N → W − 1 = N
16 peano2nn0 ⊢ N ∈ ℕ 0 → N + 1 ∈ ℕ 0
17 4 16 ax-mp ⊢ N + 1 ∈ ℕ 0
18 eleq1 ⊢ W = N + 1 → W ∈ ℕ 0 ↔ N + 1 ∈ ℕ 0
19 17 18 mpbiri ⊢ W = N + 1 → W ∈ ℕ 0
20 19 adantr ⊢ W = N + 1 ∧ G ∈ USGraph ∧ X ∈ V ∧ U = N → W ∈ ℕ 0
21 6 fvexi ⊢ W ∈ V
22 hashclb ⊢ W ∈ V → W ∈ Fin ↔ W ∈ ℕ 0
23 21 22 mp1i ⊢ W = N + 1 ∧ G ∈ USGraph ∧ X ∈ V ∧ U = N → W ∈ Fin ↔ W ∈ ℕ 0
24 20 23 mpbird ⊢ W = N + 1 ∧ G ∈ USGraph ∧ X ∈ V ∧ U = N → W ∈ Fin
25 5 6 stgrvtx0 ⊢ N ∈ ℕ 0 → 0 ∈ W
26 4 25 ax-mp ⊢ 0 ∈ W
27 hashdifsn ⊢ W ∈ Fin ∧ 0 ∈ W → W ∖ 0 = W − 1
28 24 26 27 sylancl ⊢ W = N + 1 ∧ G ∈ USGraph ∧ X ∈ V ∧ U = N → W ∖ 0 = W − 1
29 simpr3 ⊢ W = N + 1 ∧ G ∈ USGraph ∧ X ∈ V ∧ U = N → U = N
30 15 28 29 3eqtr4rd ⊢ W = N + 1 ∧ G ∈ USGraph ∧ X ∈ V ∧ U = N → U = W ∖ 0
31 eleq1 ⊢ U = N → U ∈ ℕ 0 ↔ N ∈ ℕ 0
32 4 31 mpbiri ⊢ U = N → U ∈ ℕ 0
33 32 3ad2ant3 ⊢ G ∈ USGraph ∧ X ∈ V ∧ U = N → U ∈ ℕ 0
34 2 ovexi ⊢ U ∈ V
35 hashclb ⊢ U ∈ V → U ∈ Fin ↔ U ∈ ℕ 0
36 34 35 mp1i ⊢ G ∈ USGraph ∧ X ∈ V ∧ U = N → U ∈ Fin ↔ U ∈ ℕ 0
37 33 36 mpbird ⊢ G ∈ USGraph ∧ X ∈ V ∧ U = N → U ∈ Fin
38 diffi ⊢ W ∈ Fin → W ∖ 0 ∈ Fin
39 24 38 syl ⊢ W = N + 1 ∧ G ∈ USGraph ∧ X ∈ V ∧ U = N → W ∖ 0 ∈ Fin
40 hasheqf1o ⊢ U ∈ Fin ∧ W ∖ 0 ∈ Fin → U = W ∖ 0 ↔ ∃ f f : U ⟶ 1-1 onto W ∖ 0
41 37 39 40 syl2an2 ⊢ W = N + 1 ∧ G ∈ USGraph ∧ X ∈ V ∧ U = N → U = W ∖ 0 ↔ ∃ f f : U ⟶ 1-1 onto W ∖ 0
42 30 41 mpbid ⊢ W = N + 1 ∧ G ∈ USGraph ∧ X ∈ V ∧ U = N → ∃ f f : U ⟶ 1-1 onto W ∖ 0
43 8 42 mpan ⊢ G ∈ USGraph ∧ X ∈ V ∧ U = N → ∃ f f : U ⟶ 1-1 onto W ∖ 0