isubgr3stgrlem6

	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)$
	isubgr3stgr.i	$⊢ I = Edg (G ISubGr C)$
	isubgr3stgr.h	$⊢ H = (i \in I ⟼ F [i])$
Assertion	isubgr3stgrlem6	Could not format assertion : No typesetting found for \|- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> H : I --> ( Edg ` ( StarGr ` N ) ) ) with typecode \|-

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		isubgr3stgr.i	$⊢ I = Edg (G ISubGr C)$
9		isubgr3stgr.h	$⊢ H = (i \in I ⟼ F [i])$
10		usgruhgr	$⊢ G \in USGraph \to G \in UHGraph$
11	10	adantr	$⊢ (G \in USGraph \land X \in V) \to G \in UHGraph$
12	11	adantr	$⊢ ((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \to G \in UHGraph$
13	1	clnbgrssvtx	$⊢ G ClNeighbVtx X \subseteq V$
14	3 13	eqsstri	$⊢ C \subseteq V$
15	14	a1i	$⊢ (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \to C \subseteq V$
16		eqid	$⊢ G ISubGr C = G ISubGr C$
17	1 7 16 8	isubgredg	$⊢ (G \in UHGraph \land C \subseteq V) \to (i \in I \leftrightarrow (i \in E \land i \subseteq C))$
18	12 15 17	syl2an	$⊢ (((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to (i \in I \leftrightarrow (i \in E \land i \subseteq C))$
19		f1of	$⊢ F : C \underset{1-1 onto}{⟶} W \to F : C ⟶ W$
20	5	fveq2i	Could not format ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for \|- ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) with typecode \|-
21		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 \|-
22	4 21	ax-mp	Could not format ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) : No typesetting found for \|- ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) with typecode \|-
23	6 20 22	3eqtri	$⊢ W = (0 \dots N)$
24	23	eqimssi	$⊢ W \subseteq (0 \dots N)$
25	24	a1i	$⊢ F : C \underset{1-1 onto}{⟶} W \to W \subseteq (0 \dots N)$
26	19 25	fssd	$⊢ F : C \underset{1-1 onto}{⟶} W \to F : C ⟶ (0 \dots N)$
27	26	ad2antrl	$⊢ (((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to F : C ⟶ (0 \dots N)$
28	27	adantr	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (i \in E \land i \subseteq C)) \to F : C ⟶ (0 \dots N)$
29	28	fimassd	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (i \in E \land i \subseteq C)) \to F [i] \subseteq (0 \dots N)$
30		simplll	$⊢ (((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to G \in USGraph$
31		simpl	$⊢ (i \in E \land i \subseteq C) \to i \in E$
32	1 7	usgredg	$⊢ (G \in USGraph \land i \in E) \to \exists a \in V \exists b \in V (a \neq b \land i = \{a, b\})$
33	30 31 32	syl2an	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (i \in E \land i \subseteq C)) \to \exists a \in V \exists b \in V (a \neq b \land i = \{a, b\})$
34		vex	$⊢ a \in V$
35		vex	$⊢ b \in V$
36	34 35	prss	$⊢ (a \in C \land b \in C) \leftrightarrow \{a, b\} \subseteq C$
37		elclnbgrelnbgr	$⊢ (a \in (G ClNeighbVtx X) \land a \neq X) \to a \in (G NeighbVtx X)$
38	37	expcom	$⊢ a \neq X \to (a \in (G ClNeighbVtx X) \to a \in (G NeighbVtx X))$
39	3	eleq2i	$⊢ a \in C \leftrightarrow a \in (G ClNeighbVtx X)$
40	2	eleq2i	$⊢ a \in U \leftrightarrow a \in (G NeighbVtx X)$
41	38 39 40	3imtr4g	$⊢ a \neq X \to (a \in C \to a \in U)$
42		elclnbgrelnbgr	$⊢ (b \in (G ClNeighbVtx X) \land b \neq X) \to b \in (G NeighbVtx X)$
43	42	expcom	$⊢ b \neq X \to (b \in (G ClNeighbVtx X) \to b \in (G NeighbVtx X))$
44	3	eleq2i	$⊢ b \in C \leftrightarrow b \in (G ClNeighbVtx X)$
45	2	eleq2i	$⊢ b \in U \leftrightarrow b \in (G NeighbVtx X)$
46	43 44 45	3imtr4g	$⊢ b \neq X \to (b \in C \to b \in U)$
47	41 46	im2anan9r	$⊢ (b \neq X \land a \neq X) \to ((a \in C \land b \in C) \to (a \in U \land b \in U))$
48	47	imp	$⊢ ((b \neq X \land a \neq X) \land (a \in C \land b \in C)) \to (a \in U \land b \in U)$
49	48	3adant3	$⊢ ((b \neq X \land a \neq X) \land (a \in C \land b \in C) \land (a \neq b \land \{a, b\} \in E)) \to (a \in U \land b \in U)$
50		preq1	$⊢ x = a \to \{x, y\} = \{a, y\}$
51		eqidd	$⊢ x = a \to E = E$
52	50 51	neleq12d	$⊢ x = a \to (\{x, y\} \notin E \leftrightarrow \{a, y\} \notin E)$
53		preq2	$⊢ y = b \to \{a, y\} = \{a, b\}$
54		eqidd	$⊢ y = b \to E = E$
55	53 54	neleq12d	$⊢ y = b \to (\{a, y\} \notin E \leftrightarrow \{a, b\} \notin E)$
56	52 55	rspc2v	$⊢ (a \in U \land b \in U) \to (\forall x \in U \forall y \in U \{x, y\} \notin E \to \{a, b\} \notin E)$
57	49 56	syl	$⊢ ((b \neq X \land a \neq X) \land (a \in C \land b \in C) \land (a \neq b \land \{a, b\} \in E)) \to (\forall x \in U \forall y \in U \{x, y\} \notin E \to \{a, b\} \notin E)$
58		pm2.24nel	$⊢ \{a, b\} \in E \to (\{a, b\} \notin E \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})$
59	58	adantl	$⊢ (a \neq b \land \{a, b\} \in E) \to (\{a, b\} \notin E \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})$
60	59	3ad2ant3	$⊢ ((b \neq X \land a \neq X) \land (a \in C \land b \in C) \land (a \neq b \land \{a, b\} \in E)) \to (\{a, b\} \notin E \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})$
61	57 60	syld	$⊢ ((b \neq X \land a \neq X) \land (a \in C \land b \in C) \land (a \neq b \land \{a, b\} \in E)) \to (\forall x \in U \forall y \in U \{x, y\} \notin E \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})$
62	61	3exp	$⊢ (b \neq X \land a \neq X) \to ((a \in C \land b \in C) \to ((a \neq b \land \{a, b\} \in E) \to (\forall x \in U \forall y \in U \{x, y\} \notin E \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})))$
63	62	com24	$⊢ (b \neq X \land a \neq X) \to (\forall x \in U \forall y \in U \{x, y\} \notin E \to ((a \neq b \land \{a, b\} \in E) \to ((a \in C \land b \in C) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})))$
64	63	adantld	$⊢ (b \neq X \land a \neq X) \to ((\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E) \to ((a \neq b \land \{a, b\} \in E) \to ((a \in C \land b \in C) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})))$
65	64	adantld	$⊢ (b \neq X \land a \neq X) \to (((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \to ((a \neq b \land \{a, b\} \in E) \to ((a \in C \land b \in C) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})))$
66	65	adantrd	$⊢ (b \neq X \land a \neq X) \to ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to ((a \neq b \land \{a, b\} \in E) \to ((a \in C \land b \in C) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})))$
67	66	imp4c	$⊢ (b \neq X \land a \neq X) \to ((((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C)) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})$
68		simpl	$⊢ (b = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to b = X$
69		simpllr	$⊢ (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C)) \to (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)$
70	69	adantl	$⊢ (b = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)$
71		simplrl	$⊢ (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C)) \to a \neq b$
72	71	necomd	$⊢ (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C)) \to b \neq a$
73	72	adantl	$⊢ (b = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to b \neq a$
74		simprrr	$⊢ (b = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to b \in C$
75		simprrl	$⊢ (b = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to a \in C$
76	1 2 3 4 5 6 7	isubgr3stgrlem4	$⊢ (b = X \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \land (b \neq a \land b \in C \land a \in C)) \to \exists z \in (1 \dots N) F [\{b, a\}] = \{0, z\}$
77	68 70 73 74 75 76	syl113anc	$⊢ (b = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to \exists z \in (1 \dots N) F [\{b, a\}] = \{0, z\}$
78		prcom	$⊢ \{a, b\} = \{b, a\}$
79	78	imaeq2i	$⊢ F [\{a, b\}] = F [\{b, a\}]$
80	79	eqeq1i	$⊢ F [\{a, b\}] = \{0, z\} \leftrightarrow F [\{b, a\}] = \{0, z\}$
81	80	rexbii	$⊢ \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\} \leftrightarrow \exists z \in (1 \dots N) F [\{b, a\}] = \{0, z\}$
82	77 81	sylibr	$⊢ (b = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\}$
83	82	ex	$⊢ b = X \to ((((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C)) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})$
84		simpl	$⊢ (a = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to a = X$
85	69	adantl	$⊢ (a = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)$
86	71	adantl	$⊢ (a = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to a \neq b$
87		simprrl	$⊢ (a = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to a \in C$
88		simprrr	$⊢ (a = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to b \in C$
89	1 2 3 4 5 6 7	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\}$
90	84 85 86 87 88 89	syl113anc	$⊢ (a = X \land (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C))) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\}$
91	90	ex	$⊢ a = X \to ((((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C)) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})$
92	67 83 91	pm2.61iine	$⊢ (((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \land (a \in C \land b \in C)) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\}$
93	92	ex	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \to ((a \in C \land b \in C) \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})$
94	36 93	biimtrrid	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land \{a, b\} \in E)) \to (\{a, b\} \subseteq C \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})$
95	94	exp32	$⊢ (((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to (a \neq b \to (\{a, b\} \in E \to (\{a, b\} \subseteq C \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})))$
96	95	adantrd	$⊢ (((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to ((a \neq b \land i = \{a, b\}) \to (\{a, b\} \in E \to (\{a, b\} \subseteq C \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})))$
97	96	imp	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land i = \{a, b\})) \to (\{a, b\} \in E \to (\{a, b\} \subseteq C \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\}))$
98	97	com23	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land i = \{a, b\})) \to (\{a, b\} \subseteq C \to (\{a, b\} \in E \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\}))$
99		sseq1	$⊢ i = \{a, b\} \to (i \subseteq C \leftrightarrow \{a, b\} \subseteq C)$
100		eleq1	$⊢ i = \{a, b\} \to (i \in E \leftrightarrow \{a, b\} \in E)$
101		imaeq2	$⊢ i = \{a, b\} \to F [i] = F [\{a, b\}]$
102	101	eqeq1d	$⊢ i = \{a, b\} \to (F [i] = \{0, z\} \leftrightarrow F [\{a, b\}] = \{0, z\})$
103	102	rexbidv	$⊢ i = \{a, b\} \to (\exists z \in (1 \dots N) F [i] = \{0, z\} \leftrightarrow \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})$
104	100 103	imbi12d	$⊢ i = \{a, b\} \to ((i \in E \to \exists z \in (1 \dots N) F [i] = \{0, z\}) \leftrightarrow (\{a, b\} \in E \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\}))$
105	99 104	imbi12d	$⊢ i = \{a, b\} \to ((i \subseteq C \to (i \in E \to \exists z \in (1 \dots N) F [i] = \{0, z\})) \leftrightarrow (\{a, b\} \subseteq C \to (\{a, b\} \in E \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})))$
106	105	adantl	$⊢ (a \neq b \land i = \{a, b\}) \to ((i \subseteq C \to (i \in E \to \exists z \in (1 \dots N) F [i] = \{0, z\})) \leftrightarrow (\{a, b\} \subseteq C \to (\{a, b\} \in E \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})))$
107	106	adantl	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land i = \{a, b\})) \to ((i \subseteq C \to (i \in E \to \exists z \in (1 \dots N) F [i] = \{0, z\})) \leftrightarrow (\{a, b\} \subseteq C \to (\{a, b\} \in E \to \exists z \in (1 \dots N) F [\{a, b\}] = \{0, z\})))$
108	98 107	mpbird	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (a \neq b \land i = \{a, b\})) \to (i \subseteq C \to (i \in E \to \exists z \in (1 \dots N) F [i] = \{0, z\}))$
109	108	ex	$⊢ (((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to ((a \neq b \land i = \{a, b\}) \to (i \subseteq C \to (i \in E \to \exists z \in (1 \dots N) F [i] = \{0, z\})))$
110	109	com24	$⊢ (((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to (i \in E \to (i \subseteq C \to ((a \neq b \land i = \{a, b\}) \to \exists z \in (1 \dots N) F [i] = \{0, z\})))$
111	110	imp32	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (i \in E \land i \subseteq C)) \to ((a \neq b \land i = \{a, b\}) \to \exists z \in (1 \dots N) F [i] = \{0, z\})$
112	111	a1d	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (i \in E \land i \subseteq C)) \to ((a \in V \land b \in V) \to ((a \neq b \land i = \{a, b\}) \to \exists z \in (1 \dots N) F [i] = \{0, z\}))$
113	112	rexlimdvv	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (i \in E \land i \subseteq C)) \to (\exists a \in V \exists b \in V (a \neq b \land i = \{a, b\}) \to \exists z \in (1 \dots N) F [i] = \{0, z\})$
114	33 113	mpd	$⊢ ((((G \in USGraph \land X \in V) \land (\|U\| = N \land \forall x \in U \forall y \in U \{x, y\} \notin E)) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land (i \in E \land i \subseteq C)) \to \exists z \in (1 \dots N) F [i] = \{0, z\}$
115		stgredgel	Could not format ( N e. NN0 -> ( ( F " i ) e. ( Edg ` ( StarGr ` N ) ) <-> ( ( F " i ) C_ ( 0 ... N ) /\ E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) ) : No typesetting found for \|- ( N e. NN0 -> ( ( F " i ) e. ( Edg ` ( StarGr ` N ) ) <-> ( ( F " i ) C_ ( 0 ... N ) /\ E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) ) with typecode \|-
116	4 115	ax-mp	Could not format ( ( F " i ) e. ( Edg ` ( StarGr ` N ) ) <-> ( ( F " i ) C_ ( 0 ... N ) /\ E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) : No typesetting found for \|- ( ( F " i ) e. ( Edg ` ( StarGr ` N ) ) <-> ( ( F " i ) C_ ( 0 ... N ) /\ E. z e. ( 1 ... N ) ( F " i ) = { 0 , z } ) ) with typecode \|-
117	29 114 116	sylanbrc	Could not format ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( i e. E /\ i C_ C ) ) -> ( F " i ) e. ( Edg ` ( StarGr ` N ) ) ) : No typesetting found for \|- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ ( i e. E /\ i C_ C ) ) -> ( F " i ) e. ( Edg ` ( StarGr ` N ) ) ) with typecode \|-
118	18 117	sylbida	Could not format ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ i e. I ) -> ( F " i ) e. ( Edg ` ( StarGr ` N ) ) ) : No typesetting found for \|- ( ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) /\ i e. I ) -> ( F " i ) e. ( Edg ` ( StarGr ` N ) ) ) with typecode \|-
119	118 9	fmptd	Could not format ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> H : I --> ( Edg ` ( StarGr ` N ) ) ) : No typesetting found for \|- ( ( ( ( G e. USGraph /\ X e. V ) /\ ( ( # ` U ) = N /\ A. x e. U A. y e. U { x , y } e/ E ) ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> H : I --> ( Edg ` ( StarGr ` N ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem isubgr3stgrlem6

Proof