isubgr3stgrlem4

	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)$
	isubgr3stgr.e	$⊢ E = Edg (G)$
Assertion	isubgr3stgrlem4	$⊢ (A = X \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (A \neq B \land A \in C \land B \in C)) \to \exists z \in (1 \dots N) F [\{A, B\}] = \{0, z\}$

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		isubgr3stgr.e	$⊢ E = Edg (G)$
8		preq2	$⊢ z = F (B) \to \{0, z\} = \{0, F (B)\}$
9	8	eqeq2d	$⊢ z = F (B) \to (F [\{X, B\}] = \{0, z\} \leftrightarrow F [\{X, B\}] = \{0, F (B)\})$
10		f1of	$⊢ F : C \underset{1-1 onto}{⟶} W \to F : C ⟶ W$
11	10	adantr	$⊢ (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \to F : C ⟶ W$
12	11	adantr	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to F : C ⟶ W$
13		simpr3	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to B \in C$
14	12 13	ffvelcdmd	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to F (B) \in W$
15	5	fveq2i	Could not format ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for \|- ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) with typecode \|-
16		stgrvtx	Could not format ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) : No typesetting found for \|- ( N e. NN0 -> ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) ) with typecode \|-
17	4 16	ax-mp	Could not format ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) : No typesetting found for \|- ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) with typecode \|-
18	6 15 17	3eqtri	$⊢ W = (0 \dots N)$
19	18	eleq2i	$⊢ F (B) \in W \leftrightarrow F (B) \in (0 \dots N)$
20		fz0sn0fz1	$⊢ N \in ℕ_{0} \to (0 \dots N) = \{0\} \cup (1 \dots N)$
21	4 20	ax-mp	$⊢ (0 \dots N) = \{0\} \cup (1 \dots N)$
22	21	eleq2i	$⊢ F (B) \in (0 \dots N) \leftrightarrow F (B) \in (\{0\} \cup (1 \dots N))$
23		elun	$⊢ F (B) \in (\{0\} \cup (1 \dots N)) \leftrightarrow (F (B) \in \{0\} \lor F (B) \in (1 \dots N))$
24		fvex	$⊢ F (B) \in V$
25	24	elsn	$⊢ F (B) \in \{0\} \leftrightarrow F (B) = 0$
26	25	orbi1i	$⊢ (F (B) \in \{0\} \lor F (B) \in (1 \dots N)) \leftrightarrow (F (B) = 0 \lor F (B) \in (1 \dots N))$
27	23 26	bitri	$⊢ F (B) \in (\{0\} \cup (1 \dots N)) \leftrightarrow (F (B) = 0 \lor F (B) \in (1 \dots N))$
28	19 22 27	3bitri	$⊢ F (B) \in W \leftrightarrow (F (B) = 0 \lor F (B) \in (1 \dots N))$
29		eqeq2	$⊢ F (X) = 0 \to (F (B) = F (X) \leftrightarrow F (B) = 0)$
30	29	adantl	$⊢ (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \to (F (B) = F (X) \leftrightarrow F (B) = 0)$
31	30	adantr	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to (F (B) = F (X) \leftrightarrow F (B) = 0)$
32		f1of1	$⊢ F : C \underset{1-1 onto}{⟶} W \to F : C \underset{1-1}{⟶} W$
33		dff14a	$⊢ F : C \underset{1-1}{⟶} W \leftrightarrow (F : C ⟶ W \land \forall a \in C \forall b \in C (a \neq b \to F (a) \neq F (b)))$
34		simpl	$⊢ (a = X \land b = B) \to a = X$
35		simpr	$⊢ (a = X \land b = B) \to b = B$
36	34 35	neeq12d	$⊢ (a = X \land b = B) \to (a \neq b \leftrightarrow X \neq B)$
37		fveq2	$⊢ a = X \to F (a) = F (X)$
38	37	adantr	$⊢ (a = X \land b = B) \to F (a) = F (X)$
39		fveq2	$⊢ b = B \to F (b) = F (B)$
40	39	adantl	$⊢ (a = X \land b = B) \to F (b) = F (B)$
41	38 40	neeq12d	$⊢ (a = X \land b = B) \to (F (a) \neq F (b) \leftrightarrow F (X) \neq F (B))$
42	36 41	imbi12d	$⊢ (a = X \land b = B) \to ((a \neq b \to F (a) \neq F (b)) \leftrightarrow (X \neq B \to F (X) \neq F (B)))$
43	42	rspc2gv	$⊢ (X \in C \land B \in C) \to (\forall a \in C \forall b \in C (a \neq b \to F (a) \neq F (b)) \to (X \neq B \to F (X) \neq F (B)))$
44	43	3adant1	$⊢ (X \neq B \land X \in C \land B \in C) \to (\forall a \in C \forall b \in C (a \neq b \to F (a) \neq F (b)) \to (X \neq B \to F (X) \neq F (B)))$
45		id	$⊢ (X \neq B \to F (X) \neq F (B)) \to (X \neq B \to F (X) \neq F (B))$
46		eqneqall	$⊢ F (X) = F (B) \to (F (X) \neq F (B) \to F (B) \in (1 \dots N))$
47	46	eqcoms	$⊢ F (B) = F (X) \to (F (X) \neq F (B) \to F (B) \in (1 \dots N))$
48	47	com12	$⊢ F (X) \neq F (B) \to (F (B) = F (X) \to F (B) \in (1 \dots N))$
49	45 48	syl6com	$⊢ X \neq B \to ((X \neq B \to F (X) \neq F (B)) \to (F (B) = F (X) \to F (B) \in (1 \dots N)))$
50	49	3ad2ant1	$⊢ (X \neq B \land X \in C \land B \in C) \to ((X \neq B \to F (X) \neq F (B)) \to (F (B) = F (X) \to F (B) \in (1 \dots N)))$
51	44 50	syld	$⊢ (X \neq B \land X \in C \land B \in C) \to (\forall a \in C \forall b \in C (a \neq b \to F (a) \neq F (b)) \to (F (B) = F (X) \to F (B) \in (1 \dots N)))$
52	51	adantld	$⊢ (X \neq B \land X \in C \land B \in C) \to ((F : C ⟶ W \land \forall a \in C \forall b \in C (a \neq b \to F (a) \neq F (b))) \to (F (B) = F (X) \to F (B) \in (1 \dots N)))$
53	33 52	biimtrid	$⊢ (X \neq B \land X \in C \land B \in C) \to (F : C \underset{1-1}{⟶} W \to (F (B) = F (X) \to F (B) \in (1 \dots N)))$
54	32 53	syl5com	$⊢ F : C \underset{1-1 onto}{⟶} W \to ((X \neq B \land X \in C \land B \in C) \to (F (B) = F (X) \to F (B) \in (1 \dots N)))$
55	54	adantr	$⊢ (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \to ((X \neq B \land X \in C \land B \in C) \to (F (B) = F (X) \to F (B) \in (1 \dots N)))$
56	55	imp	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to (F (B) = F (X) \to F (B) \in (1 \dots N))$
57	31 56	sylbird	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to (F (B) = 0 \to F (B) \in (1 \dots N))$
58		idd	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to (F (B) \in (1 \dots N) \to F (B) \in (1 \dots N))$
59	57 58	jaod	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to ((F (B) = 0 \lor F (B) \in (1 \dots N)) \to F (B) \in (1 \dots N))$
60	28 59	biimtrid	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to (F (B) \in W \to F (B) \in (1 \dots N))$
61	14 60	mpd	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to F (B) \in (1 \dots N)$
62		f1ofn	$⊢ F : C \underset{1-1 onto}{⟶} W \to F Fn C$
63	62	adantr	$⊢ (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \to F Fn C$
64		3simpc	$⊢ (X \neq B \land X \in C \land B \in C) \to (X \in C \land B \in C)$
65	63 64	anim12i	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to (F Fn C \land (X \in C \land B \in C))$
66		3anass	$⊢ (F Fn C \land X \in C \land B \in C) \leftrightarrow (F Fn C \land (X \in C \land B \in C))$
67	65 66	sylibr	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to (F Fn C \land X \in C \land B \in C)$
68		fnimapr	$⊢ (F Fn C \land X \in C \land B \in C) \to F [\{X, B\}] = \{F (X), F (B)\}$
69	67 68	syl	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to F [\{X, B\}] = \{F (X), F (B)\}$
70		simpr	$⊢ (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \to F (X) = 0$
71	70	adantr	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to F (X) = 0$
72	71	preq1d	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to \{F (X), F (B)\} = \{0, F (B)\}$
73	69 72	eqtrd	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to F [\{X, B\}] = \{0, F (B)\}$
74	9 61 73	rspcedvdw	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (X \neq B \land X \in C \land B \in C)) \to \exists z \in (1 \dots N) F [\{X, B\}] = \{0, z\}$
75	74	ex	$⊢ (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \to ((X \neq B \land X \in C \land B \in C) \to \exists z \in (1 \dots N) F [\{X, B\}] = \{0, z\})$
76		neeq1	$⊢ A = X \to (A \neq B \leftrightarrow X \neq B)$
77		eleq1	$⊢ A = X \to (A \in C \leftrightarrow X \in C)$
78	76 77	3anbi12d	$⊢ A = X \to ((A \neq B \land A \in C \land B \in C) \leftrightarrow (X \neq B \land X \in C \land B \in C))$
79		preq1	$⊢ A = X \to \{A, B\} = \{X, B\}$
80	79	imaeq2d	$⊢ A = X \to F [\{A, B\}] = F [\{X, B\}]$
81	80	eqeq1d	$⊢ A = X \to (F [\{A, B\}] = \{0, z\} \leftrightarrow F [\{X, B\}] = \{0, z\})$
82	81	rexbidv	$⊢ A = X \to (\exists z \in (1 \dots N) F [\{A, B\}] = \{0, z\} \leftrightarrow \exists z \in (1 \dots N) F [\{X, B\}] = \{0, z\})$
83	78 82	imbi12d	$⊢ A = X \to (((A \neq B \land A \in C \land B \in C) \to \exists z \in (1 \dots N) F [\{A, B\}] = \{0, z\}) \leftrightarrow ((X \neq B \land X \in C \land B \in C) \to \exists z \in (1 \dots N) F [\{X, B\}] = \{0, z\}))$
84	75 83	imbitrrid	$⊢ A = X \to ((F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \to ((A \neq B \land A \in C \land B \in C) \to \exists z \in (1 \dots N) F [\{A, B\}] = \{0, z\}))$
85	84	3imp	$⊢ (A = X \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (A \neq B \land A \in C \land B \in C)) \to \exists z \in (1 \dots N) F [\{A, B\}] = \{0, z\}$

Metamath Proof Explorer

Theorem isubgr3stgrlem4

Proof