isubgr3stgrlem3

	Ref	Expression
Hypotheses	isubgr3stgr.v	$⊢ V = Vtx (G)$
	isubgr3stgr.u	$⊢ U = G NeighbVtx X$
	isubgr3stgr.c	$⊢ C = G ClNeighbVtx X$
	isubgr3stgr.n	$⊢ N \in ℕ_{0}$
	isubgr3stgr.s	No typesetting found for \|- S = ( StarGr ` N ) with typecode \|-
	isubgr3stgr.w	$⊢ W = Vtx (S)$
Assertion	isubgr3stgrlem3	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to \exists g (g : C \underset{1-1 onto}{⟶} W \land g (X) = 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 \in ℕ_{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	1 2 3 4 5 6	isubgr3stgrlem2	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to \exists f f : U \underset{1-1 onto}{⟶} W ∖ \{0\}$
8		f1odm	$⊢ f : U \underset{1-1 onto}{⟶} W ∖ \{0\} \to dom f = U$
9		simpr	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land f : U \underset{1-1 onto}{⟶} W ∖ \{0\}) \to f : U \underset{1-1 onto}{⟶} W ∖ \{0\}$
10		simpl2	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land f : U \underset{1-1 onto}{⟶} W ∖ \{0\}) \to X \in V$
11		c0ex	$⊢ 0 \in V$
12	11	a1i	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land f : U \underset{1-1 onto}{⟶} W ∖ \{0\}) \to 0 \in V$
13		neldifsnd	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land f : U \underset{1-1 onto}{⟶} W ∖ \{0\}) \to \neg 0 \in (W ∖ \{0\})$
14		df-nel	$⊢ 0 \notin (W ∖ \{0\}) \leftrightarrow \neg 0 \in (W ∖ \{0\})$
15	13 14	sylibr	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land f : U \underset{1-1 onto}{⟶} W ∖ \{0\}) \to 0 \notin (W ∖ \{0\})$
16		eqid	$⊢ f \cup \{⟨X, 0⟩\} = f \cup \{⟨X, 0⟩\}$
17	1 2 3 16	isubgr3stgrlem1	$⊢ (f : U \underset{1-1 onto}{⟶} W ∖ \{0\} \land X \in V \land (0 \in V \land 0 \notin (W ∖ \{0\}))) \to (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\}$
18	9 10 12 15 17	syl112anc	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land f : U \underset{1-1 onto}{⟶} W ∖ \{0\}) \to (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\}$
19	18	ex	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to (f : U \underset{1-1 onto}{⟶} W ∖ \{0\} \to (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\})$
20		f1of	$⊢ (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \to (f \cup \{⟨X, 0⟩\}) : C ⟶ (W ∖ \{0\}) \cup \{0\}$
21	20	3ad2ant2	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to (f \cup \{⟨X, 0⟩\}) : C ⟶ (W ∖ \{0\}) \cup \{0\}$
22	3	ovexi	$⊢ C \in V$
23	22	a1i	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to C \in V$
24	21 23	fexd	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to f \cup \{⟨X, 0⟩\} \in V$
25	5 6	stgrvtx0	$⊢ N \in ℕ_{0} \to 0 \in W$
26	4 25	mp1i	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to 0 \in W$
27	26	snssd	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to \{0\} \subseteq W$
28		undifr	$⊢ \{0\} \subseteq W \leftrightarrow (W ∖ \{0\}) \cup \{0\} = W$
29	27 28	sylib	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to (W ∖ \{0\}) \cup \{0\} = W$
30	29	f1oeq3d	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to ((f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \leftrightarrow (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} W)$
31	30	biimpa	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\}) \to (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} W$
32	31	3adant3	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} W$
33		simp12	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to X \in V$
34	11	a1i	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to 0 \in V$
35		nbgrnself2	$⊢ X \notin (G NeighbVtx X)$
36		df-nel	$⊢ X \notin (G NeighbVtx X) \leftrightarrow \neg X \in (G NeighbVtx X)$
37	2	eleq2i	$⊢ X \in U \leftrightarrow X \in (G NeighbVtx X)$
38	36 37	xchbinxr	$⊢ X \notin (G NeighbVtx X) \leftrightarrow \neg X \in U$
39	35 38	mpbi	$⊢ \neg X \in U$
40		eleq2	$⊢ dom f = U \to (X \in dom f \leftrightarrow X \in U)$
41	40	notbid	$⊢ dom f = U \to (\neg X \in dom f \leftrightarrow \neg X \in U)$
42	41	3ad2ant3	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to (\neg X \in dom f \leftrightarrow \neg X \in U)$
43	39 42	mpbiri	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to \neg X \in dom f$
44		fsnunfv	$⊢ (X \in V \land 0 \in V \land \neg X \in dom f) \to (f \cup \{⟨X, 0⟩\}) (X) = 0$
45	33 34 43 44	syl3anc	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to (f \cup \{⟨X, 0⟩\}) (X) = 0$
46	32 45	jca	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to ((f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} W \land (f \cup \{⟨X, 0⟩\}) (X) = 0)$
47		f1oeq1	$⊢ g = f \cup \{⟨X, 0⟩\} \to (g : C \underset{1-1 onto}{⟶} W \leftrightarrow (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} W)$
48		fveq1	$⊢ g = f \cup \{⟨X, 0⟩\} \to g (X) = (f \cup \{⟨X, 0⟩\}) (X)$
49	48	eqeq1d	$⊢ g = f \cup \{⟨X, 0⟩\} \to (g (X) = 0 \leftrightarrow (f \cup \{⟨X, 0⟩\}) (X) = 0)$
50	47 49	anbi12d	$⊢ g = f \cup \{⟨X, 0⟩\} \to ((g : C \underset{1-1 onto}{⟶} W \land g (X) = 0) \leftrightarrow ((f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} W \land (f \cup \{⟨X, 0⟩\}) (X) = 0))$
51	24 46 50	spcedv	$⊢ ((G \in USGraph \land X \in V \land \|U\| = N) \land (f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \land dom f = U) \to \exists g (g : C \underset{1-1 onto}{⟶} W \land g (X) = 0)$
52	51	3exp	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to ((f \cup \{⟨X, 0⟩\}) : C \underset{1-1 onto}{⟶} (W ∖ \{0\}) \cup \{0\} \to (dom f = U \to \exists g (g : C \underset{1-1 onto}{⟶} W \land g (X) = 0)))$
53	19 52	syld	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to (f : U \underset{1-1 onto}{⟶} W ∖ \{0\} \to (dom f = U \to \exists g (g : C \underset{1-1 onto}{⟶} W \land g (X) = 0)))$
54	8 53	mpdi	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to (f : U \underset{1-1 onto}{⟶} W ∖ \{0\} \to \exists g (g : C \underset{1-1 onto}{⟶} W \land g (X) = 0))$
55	54	exlimdv	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to (\exists f f : U \underset{1-1 onto}{⟶} W ∖ \{0\} \to \exists g (g : C \underset{1-1 onto}{⟶} W \land g (X) = 0))$
56	7 55	mpd	$⊢ (G \in USGraph \land X \in V \land \|U\| = N) \to \exists g (g : C \underset{1-1 onto}{⟶} W \land g (X) = 0)$

Metamath Proof Explorer

Theorem isubgr3stgrlem3

Proof