isubgr3stgrlem7

	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	isubgr3stgrlem7	Could not format assertion : No typesetting found for \|- ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ J e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " J ) e. I ) 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		stgredgel	Could not format ( N e. NN0 -> ( J e. ( Edg ` ( StarGr ` N ) ) <-> ( J C_ ( 0 ... N ) /\ E. y e. ( 1 ... N ) J = { 0 , y } ) ) ) : No typesetting found for \|- ( N e. NN0 -> ( J e. ( Edg ` ( StarGr ` N ) ) <-> ( J C_ ( 0 ... N ) /\ E. y e. ( 1 ... N ) J = { 0 , y } ) ) ) with typecode \|-
11	4 10	mp1i	Could not format ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( J e. ( Edg ` ( StarGr ` N ) ) <-> ( J C_ ( 0 ... N ) /\ E. y e. ( 1 ... N ) J = { 0 , y } ) ) ) : No typesetting found for \|- ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( J e. ( Edg ` ( StarGr ` N ) ) <-> ( J C_ ( 0 ... N ) /\ E. y e. ( 1 ... N ) J = { 0 , y } ) ) ) with typecode \|-
12		c0ex	$⊢ 0 \in V$
13	12	a1i	$⊢ ((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to 0 \in V$
14		prssg	$⊢ (0 \in V \land y \in (1 \dots N)) \to ((0 \in (0 \dots N) \land y \in (0 \dots N)) \leftrightarrow \{0, y\} \subseteq (0 \dots N))$
15	13 14	sylan	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to ((0 \in (0 \dots N) \land y \in (0 \dots N)) \leftrightarrow \{0, y\} \subseteq (0 \dots N))$
16		f1ocnv	$⊢ F : C \underset{1-1 onto}{⟶} W \to F^{-1} : W \underset{1-1 onto}{⟶} C$
17		f1ofn	$⊢ F^{-1} : W \underset{1-1 onto}{⟶} C \to F^{-1} Fn W$
18	5	fveq2i	Could not format ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) : No typesetting found for \|- ( Vtx ` S ) = ( Vtx ` ( StarGr ` N ) ) with typecode \|-
19		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 \|-
20	4 19	ax-mp	Could not format ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) : No typesetting found for \|- ( Vtx ` ( StarGr ` N ) ) = ( 0 ... N ) with typecode \|-
21	6 18 20	3eqtri	$⊢ W = (0 \dots N)$
22	21	fneq2i	$⊢ F^{-1} Fn W \leftrightarrow F^{-1} Fn (0 \dots N)$
23	17 22	sylib	$⊢ F^{-1} : W \underset{1-1 onto}{⟶} C \to F^{-1} Fn (0 \dots N)$
24	16 23	syl	$⊢ F : C \underset{1-1 onto}{⟶} W \to F^{-1} Fn (0 \dots N)$
25	24	ad2antrl	$⊢ ((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to F^{-1} Fn (0 \dots N)$
26	25	adantr	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to F^{-1} Fn (0 \dots N)$
27	26	anim1i	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land (0 \in (0 \dots N) \land y \in (0 \dots N))) \to (F^{-1} Fn (0 \dots N) \land (0 \in (0 \dots N) \land y \in (0 \dots N)))$
28		3anass	$⊢ (F^{-1} Fn (0 \dots N) \land 0 \in (0 \dots N) \land y \in (0 \dots N)) \leftrightarrow (F^{-1} Fn (0 \dots N) \land (0 \in (0 \dots N) \land y \in (0 \dots N)))$
29	27 28	sylibr	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land (0 \in (0 \dots N) \land y \in (0 \dots N))) \to (F^{-1} Fn (0 \dots N) \land 0 \in (0 \dots N) \land y \in (0 \dots N))$
30	29	ex	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to ((0 \in (0 \dots N) \land y \in (0 \dots N)) \to (F^{-1} Fn (0 \dots N) \land 0 \in (0 \dots N) \land y \in (0 \dots N)))$
31	15 30	sylbird	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to (\{0, y\} \subseteq (0 \dots N) \to (F^{-1} Fn (0 \dots N) \land 0 \in (0 \dots N) \land y \in (0 \dots N)))$
32	31	imp	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land \{0, y\} \subseteq (0 \dots N)) \to (F^{-1} Fn (0 \dots N) \land 0 \in (0 \dots N) \land y \in (0 \dots N))$
33		fnimapr	$⊢ (F^{-1} Fn (0 \dots N) \land 0 \in (0 \dots N) \land y \in (0 \dots N)) \to F^{-1} [\{0, y\}] = \{F^{-1} (0), F^{-1} (y)\}$
34	32 33	syl	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land \{0, y\} \subseteq (0 \dots N)) \to F^{-1} [\{0, y\}] = \{F^{-1} (0), F^{-1} (y)\}$
35	1	clnbgrvtxel	$⊢ X \in V \to X \in (G ClNeighbVtx X)$
36	35	adantl	$⊢ (G \in USGraph \land X \in V) \to X \in (G ClNeighbVtx X)$
37	36 3	eleqtrrdi	$⊢ (G \in USGraph \land X \in V) \to X \in C$
38		simpl	$⊢ (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0) \to F : C \underset{1-1 onto}{⟶} W$
39	37 38	anim12ci	$⊢ ((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to (F : C \underset{1-1 onto}{⟶} W \land X \in C)$
40		simprr	$⊢ ((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to F (X) = 0$
41	39 40	jca	$⊢ ((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to ((F : C \underset{1-1 onto}{⟶} W \land X \in C) \land F (X) = 0)$
42	41	adantr	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to ((F : C \underset{1-1 onto}{⟶} W \land X \in C) \land F (X) = 0)$
43		f1ocnvfv	$⊢ (F : C \underset{1-1 onto}{⟶} W \land X \in C) \to (F (X) = 0 \to F^{-1} (0) = X)$
44	43	imp	$⊢ ((F : C \underset{1-1 onto}{⟶} W \land X \in C) \land F (X) = 0) \to F^{-1} (0) = X$
45	42 44	syl	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to F^{-1} (0) = X$
46	35 3	eleqtrrdi	$⊢ X \in V \to X \in C$
47	46	ad3antlr	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to X \in C$
48		f1of	$⊢ F^{-1} : W \underset{1-1 onto}{⟶} C \to F^{-1} : W ⟶ C$
49	16 48	syl	$⊢ F : C \underset{1-1 onto}{⟶} W \to F^{-1} : W ⟶ C$
50	49	ad2antrl	$⊢ ((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to F^{-1} : W ⟶ C$
51	50	adantr	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to F^{-1} : W ⟶ C$
52		fz1ssfz0	$⊢ (1 \dots N) \subseteq (0 \dots N)$
53	52	sseli	$⊢ y \in (1 \dots N) \to y \in (0 \dots N)$
54	53 21	eleqtrrdi	$⊢ y \in (1 \dots N) \to y \in W$
55	54	adantl	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to y \in W$
56	51 55	ffvelcdmd	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to F^{-1} (y) \in C$
57	47 56	jca	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to (X \in C \land F^{-1} (y) \in C)$
58	3	eleq2i	$⊢ F^{-1} (y) \in C \leftrightarrow F^{-1} (y) \in (G ClNeighbVtx X)$
59		usgrupgr	$⊢ G \in USGraph \to G \in UPGraph$
60	59	anim1i	$⊢ (G \in USGraph \land X \in V) \to (G \in UPGraph \land X \in V)$
61	60	ad2antrr	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to (G \in UPGraph \land X \in V)$
62	1	clnbgrssvtx	$⊢ G ClNeighbVtx X \subseteq V$
63	3 62	eqsstri	$⊢ C \subseteq V$
64	63 56	sselid	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to F^{-1} (y) \in V$
65		df-3an	$⊢ (G \in UPGraph \land X \in V \land F^{-1} (y) \in V) \leftrightarrow ((G \in UPGraph \land X \in V) \land F^{-1} (y) \in V)$
66	61 64 65	sylanbrc	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to (G \in UPGraph \land X \in V \land F^{-1} (y) \in V)$
67	66	ad2antrr	$⊢ (((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \land X \in C) \to (G \in UPGraph \land X \in V \land F^{-1} (y) \in V)$
68	1 7	clnbupgrel	$⊢ (G \in UPGraph \land X \in V \land F^{-1} (y) \in V) \to (F^{-1} (y) \in (G ClNeighbVtx X) \leftrightarrow (F^{-1} (y) = X \lor \{F^{-1} (y), X\} \in E))$
69	67 68	syl	$⊢ (((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \land X \in C) \to (F^{-1} (y) \in (G ClNeighbVtx X) \leftrightarrow (F^{-1} (y) = X \lor \{F^{-1} (y), X\} \in E))$
70	58 69	bitrid	$⊢ (((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \land X \in C) \to (F^{-1} (y) \in C \leftrightarrow (F^{-1} (y) = X \lor \{F^{-1} (y), X\} \in E))$
71		eqeq2	$⊢ F^{-1} (0) = X \to (F^{-1} (y) = F^{-1} (0) \leftrightarrow F^{-1} (y) = X)$
72	71	adantl	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \to (F^{-1} (y) = F^{-1} (0) \leftrightarrow F^{-1} (y) = X)$
73		f1of1	$⊢ F^{-1} : W \underset{1-1 onto}{⟶} C \to F^{-1} : W \underset{1-1}{⟶} C$
74	16 73	syl	$⊢ F : C \underset{1-1 onto}{⟶} W \to F^{-1} : W \underset{1-1}{⟶} C$
75	74	ad2antrl	$⊢ ((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to F^{-1} : W \underset{1-1}{⟶} C$
76		0elfz	$⊢ N \in ℕ_{0} \to 0 \in (0 \dots N)$
77	4 76	ax-mp	$⊢ 0 \in (0 \dots N)$
78	77 21	eleqtrri	$⊢ 0 \in W$
79	54 78	jctir	$⊢ y \in (1 \dots N) \to (y \in W \land 0 \in W)$
80		f1veqaeq	$⊢ (F^{-1} : W \underset{1-1}{⟶} C \land (y \in W \land 0 \in W)) \to (F^{-1} (y) = F^{-1} (0) \to y = 0)$
81	75 79 80	syl2an	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to (F^{-1} (y) = F^{-1} (0) \to y = 0)$
82		elfznn	$⊢ y \in (1 \dots N) \to y \in ℕ$
83		nnne0	$⊢ y \in ℕ \to y \neq 0$
84		eqneqall	$⊢ y = 0 \to (y \neq 0 \to \{X, F^{-1} (y)\} \in E)$
85	83 84	syl5com	$⊢ y \in ℕ \to (y = 0 \to \{X, F^{-1} (y)\} \in E)$
86	82 85	syl	$⊢ y \in (1 \dots N) \to (y = 0 \to \{X, F^{-1} (y)\} \in E)$
87	86	adantl	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to (y = 0 \to \{X, F^{-1} (y)\} \in E)$
88	81 87	syld	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to (F^{-1} (y) = F^{-1} (0) \to \{X, F^{-1} (y)\} \in E)$
89	88	adantr	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \to (F^{-1} (y) = F^{-1} (0) \to \{X, F^{-1} (y)\} \in E)$
90	72 89	sylbird	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \to (F^{-1} (y) = X \to \{X, F^{-1} (y)\} \in E)$
91	90	adantr	$⊢ (((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \land X \in C) \to (F^{-1} (y) = X \to \{X, F^{-1} (y)\} \in E)$
92		prcom	$⊢ \{F^{-1} (y), X\} = \{X, F^{-1} (y)\}$
93	92	eleq1i	$⊢ \{F^{-1} (y), X\} \in E \leftrightarrow \{X, F^{-1} (y)\} \in E$
94	93	biimpi	$⊢ \{F^{-1} (y), X\} \in E \to \{X, F^{-1} (y)\} \in E$
95	94	a1i	$⊢ (((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \land X \in C) \to (\{F^{-1} (y), X\} \in E \to \{X, F^{-1} (y)\} \in E)$
96	91 95	jaod	$⊢ (((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \land X \in C) \to ((F^{-1} (y) = X \lor \{F^{-1} (y), X\} \in E) \to \{X, F^{-1} (y)\} \in E)$
97	70 96	sylbid	$⊢ (((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \land X \in C) \to (F^{-1} (y) \in C \to \{X, F^{-1} (y)\} \in E)$
98	97	impr	$⊢ (((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \land (X \in C \land F^{-1} (y) \in C)) \to \{X, F^{-1} (y)\} \in E$
99		prssi	$⊢ (X \in C \land F^{-1} (y) \in C) \to \{X, F^{-1} (y)\} \subseteq C$
100	99	adantl	$⊢ (((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \land (X \in C \land F^{-1} (y) \in C)) \to \{X, F^{-1} (y)\} \subseteq C$
101	98 100	jca	$⊢ (((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \land (X \in C \land F^{-1} (y) \in C)) \to (\{X, F^{-1} (y)\} \in E \land \{X, F^{-1} (y)\} \subseteq C)$
102	57 101	mpidan	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \to (\{X, F^{-1} (y)\} \in E \land \{X, F^{-1} (y)\} \subseteq C)$
103		preq1	$⊢ F^{-1} (0) = X \to \{F^{-1} (0), F^{-1} (y)\} = \{X, F^{-1} (y)\}$
104	103	eleq1d	$⊢ F^{-1} (0) = X \to (\{F^{-1} (0), F^{-1} (y)\} \in E \leftrightarrow \{X, F^{-1} (y)\} \in E)$
105	103	sseq1d	$⊢ F^{-1} (0) = X \to (\{F^{-1} (0), F^{-1} (y)\} \subseteq C \leftrightarrow \{X, F^{-1} (y)\} \subseteq C)$
106	104 105	anbi12d	$⊢ F^{-1} (0) = X \to ((\{F^{-1} (0), F^{-1} (y)\} \in E \land \{F^{-1} (0), F^{-1} (y)\} \subseteq C) \leftrightarrow (\{X, F^{-1} (y)\} \in E \land \{X, F^{-1} (y)\} \subseteq C))$
107	106	adantl	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \to ((\{F^{-1} (0), F^{-1} (y)\} \in E \land \{F^{-1} (0), F^{-1} (y)\} \subseteq C) \leftrightarrow (\{X, F^{-1} (y)\} \in E \land \{X, F^{-1} (y)\} \subseteq C))$
108	102 107	mpbird	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land F^{-1} (0) = X) \to (\{F^{-1} (0), F^{-1} (y)\} \in E \land \{F^{-1} (0), F^{-1} (y)\} \subseteq C)$
109	45 108	mpdan	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to (\{F^{-1} (0), F^{-1} (y)\} \in E \land \{F^{-1} (0), F^{-1} (y)\} \subseteq C)$
110	109	adantr	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land \{0, y\} \subseteq (0 \dots N)) \to (\{F^{-1} (0), F^{-1} (y)\} \in E \land \{F^{-1} (0), F^{-1} (y)\} \subseteq C)$
111		usgruhgr	$⊢ G \in USGraph \to G \in UHGraph$
112	111	ad3antrrr	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to G \in UHGraph$
113	63	a1i	$⊢ \{0, y\} \subseteq (0 \dots N) \to C \subseteq V$
114		eqid	$⊢ G ISubGr C = G ISubGr C$
115	1 7 114 8	isubgredg	$⊢ (G \in UHGraph \land C \subseteq V) \to (\{F^{-1} (0), F^{-1} (y)\} \in I \leftrightarrow (\{F^{-1} (0), F^{-1} (y)\} \in E \land \{F^{-1} (0), F^{-1} (y)\} \subseteq C))$
116	112 113 115	syl2an	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land \{0, y\} \subseteq (0 \dots N)) \to (\{F^{-1} (0), F^{-1} (y)\} \in I \leftrightarrow (\{F^{-1} (0), F^{-1} (y)\} \in E \land \{F^{-1} (0), F^{-1} (y)\} \subseteq C))$
117	110 116	mpbird	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land \{0, y\} \subseteq (0 \dots N)) \to \{F^{-1} (0), F^{-1} (y)\} \in I$
118	34 117	eqeltrd	$⊢ ((((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \land \{0, y\} \subseteq (0 \dots N)) \to F^{-1} [\{0, y\}] \in I$
119	118	ex	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to (\{0, y\} \subseteq (0 \dots N) \to F^{-1} [\{0, y\}] \in I)$
120		sseq1	$⊢ J = \{0, y\} \to (J \subseteq (0 \dots N) \leftrightarrow \{0, y\} \subseteq (0 \dots N))$
121		imaeq2	$⊢ J = \{0, y\} \to F^{-1} [J] = F^{-1} [\{0, y\}]$
122	121	eleq1d	$⊢ J = \{0, y\} \to (F^{-1} [J] \in I \leftrightarrow F^{-1} [\{0, y\}] \in I)$
123	120 122	imbi12d	$⊢ J = \{0, y\} \to ((J \subseteq (0 \dots N) \to F^{-1} [J] \in I) \leftrightarrow (\{0, y\} \subseteq (0 \dots N) \to F^{-1} [\{0, y\}] \in I))$
124	119 123	syl5ibrcom	$⊢ (((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \land y \in (1 \dots N)) \to (J = \{0, y\} \to (J \subseteq (0 \dots N) \to F^{-1} [J] \in I))$
125	124	rexlimdva	$⊢ ((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to (\exists y \in (1 \dots N) J = \{0, y\} \to (J \subseteq (0 \dots N) \to F^{-1} [J] \in I))$
126	125	impcomd	$⊢ ((G \in USGraph \land X \in V) \land (F : C \underset{1-1 onto}{⟶} W \land F (X) = 0)) \to ((J \subseteq (0 \dots N) \land \exists y \in (1 \dots N) J = \{0, y\}) \to F^{-1} [J] \in I)$
127	11 126	sylbid	Could not format ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( J e. ( Edg ` ( StarGr ` N ) ) -> ( `' F " J ) e. I ) ) : No typesetting found for \|- ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) ) -> ( J e. ( Edg ` ( StarGr ` N ) ) -> ( `' F " J ) e. I ) ) with typecode \|-
128	127	3impia	Could not format ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ J e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " J ) e. I ) : No typesetting found for \|- ( ( ( G e. USGraph /\ X e. V ) /\ ( F : C -1-1-onto-> W /\ ( F ` X ) = 0 ) /\ J e. ( Edg ` ( StarGr ` N ) ) ) -> ( `' F " J ) e. I ) with typecode \|-

Metamath Proof Explorer

Theorem isubgr3stgrlem7

Proof