isubgr3stgrlem7 - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > isubgr3stgrlem7		Structured version Visualization version GIF version

Theorem isubgr3stgrlem7 48464

Description: Lemma 7 for isubgr3stgr 48467. (Contributed by AV, 29-Sep-2025.)

**Hypotheses**
Ref	Expression
isubgr3stgr.v	⊢ 𝑉 = (Vtx‘𝐺)
isubgr3stgr.u	⊢ 𝑈 = (𝐺 NeighbVtx 𝑋)
isubgr3stgr.c	⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)
isubgr3stgr.n	⊢ 𝑁 ∈ ℕ₀
isubgr3stgr.s	⊢ 𝑆 = (StarGr‘𝑁)
isubgr3stgr.w	⊢ 𝑊 = (Vtx‘𝑆)
isubgr3stgr.e	⊢ 𝐸 = (Edg‘𝐺)
isubgr3stgr.i	⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))
isubgr3stgr.h	⊢ 𝐻 = (𝑖 ∈ 𝐼 ↦ (𝐹 “ 𝑖))

**Assertion**
Ref	Expression
isubgr3stgrlem7	⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (^◡𝐹 “ 𝐽) ∈ 𝐼)

Distinct variable groups: 𝐶,𝑖 𝑖,𝐹 𝑖,𝐼 𝑖,𝑊 𝑖,𝐸 𝑖,𝐺 𝑖,𝑁 𝑈,𝑖 𝑖,𝑉 𝑖,𝑋 Allowed substitution hints: 𝑆(𝑖) 𝐻(𝑖) 𝐽(𝑖)

Proof of Theorem isubgr3stgrlem7 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isubgr3stgr.n	. . . 4 ⊢ 𝑁 ∈ ℕ₀
2		stgredgel 48449	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦})))
3	1, 2	mp1i 13	. . 3 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦})))
4		c0ex 11133	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
5	4	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 0 ∈ V)
6		prssg 4763	. . . . . . . . . . . 12 ⊢ ((0 ∈ V ∧ 𝑦 ∈ (1...𝑁)) → ((0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ {0, 𝑦} ⊆ (0...𝑁)))
7	5, 6	sylan 581	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ {0, 𝑦} ⊆ (0...𝑁)))
8		f1ocnv 6788	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶–1-1-onto→𝑊 → ^◡𝐹:𝑊–1-1-onto→𝐶)
9		f1ofn 6777	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹:𝑊–1-1-onto→𝐶 → ^◡𝐹 Fn 𝑊)
10		isubgr3stgr.w	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑊 = (Vtx‘𝑆)
11		isubgr3stgr.s	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = (StarGr‘𝑁)
12	11	fveq2i 6839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Vtx‘𝑆) = (Vtx‘(StarGr‘𝑁))
13		stgrvtx 48446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → (Vtx‘(StarGr‘𝑁)) = (0...𝑁))
14	1, 13	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Vtx‘(StarGr‘𝑁)) = (0...𝑁)
15	10, 12, 14	3eqtri 2764	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑊 = (0...𝑁)
16	15	fneq2i 6592	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹 Fn 𝑊 ↔ ^◡𝐹 Fn (0...𝑁))
17	9, 16	sylib 218	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝐹:𝑊–1-1-onto→𝐶 → ^◡𝐹 Fn (0...𝑁))
18	8, 17	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐶–1-1-onto→𝑊 → ^◡𝐹 Fn (0...𝑁))
19	18	ad2antrl 729	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ^◡𝐹 Fn (0...𝑁))
20	19	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ^◡𝐹 Fn (0...𝑁))
21	20	anim1i 616	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))) → (^◡𝐹 Fn (0...𝑁) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))))
22		3anass 1095	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ (^◡𝐹 Fn (0...𝑁) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))))
23	21, 22	sylibr 234	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))) → (^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)))
24	23	ex 412	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) → (^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))))
25	7, 24	sylbird 260	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ({0, 𝑦} ⊆ (0...𝑁) → (^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))))
26	25	imp 406	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → (^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)))
27		fnimapr 6919	. . . . . . . . 9 ⊢ ((^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) → (^◡𝐹 “ {0, 𝑦}) = {(^◡𝐹‘0), (^◡𝐹‘𝑦)})
28	26, 27	syl 17	. . . . . . . 8 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → (^◡𝐹 “ {0, 𝑦}) = {(^◡𝐹‘0), (^◡𝐹‘𝑦)})
29		isubgr3stgr.v	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑉 = (Vtx‘𝐺)
30	29	clnbgrvtxel 48321	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
31	30	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
32		isubgr3stgr.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)
33	31, 32	eleqtrrdi 2848	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝐶)
34		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → 𝐹:𝐶–1-1-onto→𝑊)
35	33, 34	anim12ci 615	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶))
36		simprr 773	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐹‘𝑋) = 0)
37	35, 36	jca 511	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ((𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶) ∧ (𝐹‘𝑋) = 0))
38	37	adantr 480	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶) ∧ (𝐹‘𝑋) = 0))
39		f1ocnvfv 7228	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶) → ((𝐹‘𝑋) = 0 → (^◡𝐹‘0) = 𝑋))
40	39	imp 406	. . . . . . . . . . . 12 ⊢ (((𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶) ∧ (𝐹‘𝑋) = 0) → (^◡𝐹‘0) = 𝑋)
41	38, 40	syl 17	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (^◡𝐹‘0) = 𝑋)
42	30, 32	eleqtrrdi 2848	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝐶)
43	42	ad3antlr 732	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑋 ∈ 𝐶)
44		f1of 6776	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹:𝑊–1-1-onto→𝐶 → ^◡𝐹:𝑊⟶𝐶)
45	8, 44	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶–1-1-onto→𝑊 → ^◡𝐹:𝑊⟶𝐶)
46	45	ad2antrl 729	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ^◡𝐹:𝑊⟶𝐶)
47	46	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ^◡𝐹:𝑊⟶𝐶)
48		fz1ssfz0 13572	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑁) ⊆ (0...𝑁)
49	48	sseli 3918	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ (0...𝑁))
50	49, 15	eleqtrrdi 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ 𝑊)
51	50	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑦 ∈ 𝑊)
52	47, 51	ffvelcdmd 7033	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (^◡𝐹‘𝑦) ∈ 𝐶)
53	43, 52	jca 511	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶))
54	32	eleq2i 2829	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝐹‘𝑦) ∈ 𝐶 ↔ (^◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋))
55		usgrupgr 29272	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph)
56	55	anim1i 616	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉))
57	56	ad2antrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉))
58	29	clnbgrssvtx 48323	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉
59	32, 58	eqsstri 3969	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐶 ⊆ 𝑉
60	59, 52	sselid 3920	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (^◡𝐹‘𝑦) ∈ 𝑉)
61		df-3an 1089	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉) ↔ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉) ∧ (^◡𝐹‘𝑦) ∈ 𝑉))
62	57, 60, 61	sylanbrc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉))
63	62	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉))
64		isubgr3stgr.e	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐸 = (Edg‘𝐺)
65	29, 64	clnbupgrel 48326	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉) → ((^◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((^◡𝐹‘𝑦) = 𝑋 ∨ {(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸)))
66	63, 65	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((^◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((^◡𝐹‘𝑦) = 𝑋 ∨ {(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸)))
67	54, 66	bitrid 283	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((^◡𝐹‘𝑦) ∈ 𝐶 ↔ ((^◡𝐹‘𝑦) = 𝑋 ∨ {(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸)))
68		eqeq2 2749	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((^◡𝐹‘0) = 𝑋 → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) ↔ (^◡𝐹‘𝑦) = 𝑋))
69	68	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) ↔ (^◡𝐹‘𝑦) = 𝑋))
70		f1of1 6775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (^◡𝐹:𝑊–1-1-onto→𝐶 → ^◡𝐹:𝑊–1-1→𝐶)
71	8, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐶–1-1-onto→𝑊 → ^◡𝐹:𝑊–1-1→𝐶)
72	71	ad2antrl 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ^◡𝐹:𝑊–1-1→𝐶)
73		0elfz 13573	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ₀ → 0 ∈ (0...𝑁))
74	1, 73	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ (0...𝑁)
75	74, 15	eleqtrri 2836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ 𝑊
76	50, 75	jctir 520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑁) → (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊))
77		f1veqaeq 7206	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((^◡𝐹:𝑊–1-1→𝐶 ∧ (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → 𝑦 = 0))
78	72, 76, 77	syl2an 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → 𝑦 = 0))
79		elfznn 13502	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
80		nnne0 12206	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0)
81		eqneqall 2944	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 0 → (𝑦 ≠ 0 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
82	80, 81	syl5com 31	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ → (𝑦 = 0 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
83	79, 82	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑁) → (𝑦 = 0 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
84	83	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝑦 = 0 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
85	78, 84	syld 47	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
86	85	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
87	69, 86	sylbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ((^◡𝐹‘𝑦) = 𝑋 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
88	87	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((^◡𝐹‘𝑦) = 𝑋 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
89		prcom 4677	. . . . . . . . . . . . . . . . . . . 20 ⊢ {(^◡𝐹‘𝑦), 𝑋} = {𝑋, (^◡𝐹‘𝑦)}
90	89	eleq1i 2828	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸 ↔ {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸)
91	90	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ ({(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸)
92	91	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ({(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
93	88, 92	jaod 860	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → (((^◡𝐹‘𝑦) = 𝑋 ∨ {(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸) → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
94	67, 93	sylbid 240	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((^◡𝐹‘𝑦) ∈ 𝐶 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
95	94	impr 454	. . . . . . . . . . . . . 14 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ (𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶)) → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸)
96		prssi 4765	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶) → {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶)
97	96	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ (𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶)) → {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶)
98	95, 97	jca 511	. . . . . . . . . . . . 13 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ (𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶)) → ({𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶))
99	53, 98	mpidan 690	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ({𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶))
100		preq1 4678	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹‘0) = 𝑋 → {(^◡𝐹‘0), (^◡𝐹‘𝑦)} = {𝑋, (^◡𝐹‘𝑦)})
101	100	eleq1d 2822	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘0) = 𝑋 → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ↔ {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
102	100	sseq1d 3954	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘0) = 𝑋 → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶 ↔ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶))
103	101, 102	anbi12d 633	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘0) = 𝑋 → (({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶) ↔ ({𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶)))
104	103	adantl 481	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → (({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶) ↔ ({𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶)))
105	99, 104	mpbird 257	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶))
106	41, 105	mpdan 688	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶))
107	106	adantr 480	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶))
108		usgruhgr 29273	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
109	108	ad3antrrr 731	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝐺 ∈ UHGraph)
110	59	a1i 11	. . . . . . . . . 10 ⊢ ({0, 𝑦} ⊆ (0...𝑁) → 𝐶 ⊆ 𝑉)
111		eqid 2737	. . . . . . . . . . 11 ⊢ (𝐺 ISubGr 𝐶) = (𝐺 ISubGr 𝐶)
112		isubgr3stgr.i	. . . . . . . . . . 11 ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))
113	29, 64, 111, 112	isubgredg 48358	. . . . . . . . . 10 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐶 ⊆ 𝑉) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐼 ↔ ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶)))
114	109, 110, 113	syl2an 597	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐼 ↔ ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶)))
115	107, 114	mpbird 257	. . . . . . . 8 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐼)
116	28, 115	eqeltrd 2837	. . . . . . 7 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → (^◡𝐹 “ {0, 𝑦}) ∈ 𝐼)
117	116	ex 412	. . . . . 6 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ({0, 𝑦} ⊆ (0...𝑁) → (^◡𝐹 “ {0, 𝑦}) ∈ 𝐼))
118		sseq1 3948	. . . . . . 7 ⊢ (𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) ↔ {0, 𝑦} ⊆ (0...𝑁)))
119		imaeq2 6017	. . . . . . . 8 ⊢ (𝐽 = {0, 𝑦} → (^◡𝐹 “ 𝐽) = (^◡𝐹 “ {0, 𝑦}))
120	119	eleq1d 2822	. . . . . . 7 ⊢ (𝐽 = {0, 𝑦} → ((^◡𝐹 “ 𝐽) ∈ 𝐼 ↔ (^◡𝐹 “ {0, 𝑦}) ∈ 𝐼))
121	118, 120	imbi12d 344	. . . . . 6 ⊢ (𝐽 = {0, 𝑦} → ((𝐽 ⊆ (0...𝑁) → (^◡𝐹 “ 𝐽) ∈ 𝐼) ↔ ({0, 𝑦} ⊆ (0...𝑁) → (^◡𝐹 “ {0, 𝑦}) ∈ 𝐼)))
122	117, 121	syl5ibrcom 247	. . . . 5 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) → (^◡𝐹 “ 𝐽) ∈ 𝐼)))
123	122	rexlimdva 3139	. . . 4 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) → (^◡𝐹 “ 𝐽) ∈ 𝐼)))
124	123	impcomd 411	. . 3 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ((𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦}) → (^◡𝐹 “ 𝐽) ∈ 𝐼))
125	3, 124	sylbid 240	. 2 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) → (^◡𝐹 “ 𝐽) ∈ 𝐼))
126	125	3impia 1118	1 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (^◡𝐹 “ 𝐽) ∈ 𝐼)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ∃wrex 3062 Vcvv 3430 ⊆ wss 3890 {cpr 4570 ↦ cmpt 5167 ^◡ccnv 5625 “ cima 5629 Fn wfn 6489 ⟶wf 6490 –1-1→wf1 6491 –1-1-onto→wf1o 6493 ‘cfv 6494 (class class class)co 7362 0cc0 11033 1c1 11034 ℕcn 12169 ℕ₀cn0 12432 ...cfz 13456 Vtxcvtx 29083 Edgcedg 29134 UHGraphcuhgr 29143 UPGraphcupgr 29167 USGraphcusgr 29236 NeighbVtx cnbgr 29419 ClNeighbVtx cclnbgr 48310 ISubGr cisubgr 48352 StarGrcstgr 48443

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5304 ax-pr 5372 ax-un 7684 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5521 df-eprel 5526 df-po 5534 df-so 5535 df-fr 5579 df-we 5581 df-xp 5632 df-rel 5633 df-cnv 5634 df-co 5635 df-dm 5636 df-rn 5637 df-res 5638 df-ima 5639 df-pred 6261 df-ord 6322 df-on 6323 df-lim 6324 df-suc 6325 df-iota 6450 df-fun 6496 df-fn 6497 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501 df-fv 6502 df-riota 7319 df-ov 7365 df-oprab 7366 df-mpo 7367 df-om 7813 df-1st 7937 df-2nd 7938 df-frecs 8226 df-wrecs 8257 df-recs 8306 df-rdg 8344 df-1o 8400 df-2o 8401 df-oadd 8404 df-er 8638 df-en 8889 df-dom 8890 df-sdom 8891 df-fin 8892 df-dju 9820 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 df-7 12244 df-8 12245 df-9 12246 df-n0 12433 df-xnn0 12506 df-z 12520 df-dec 12640 df-uz 12784 df-fz 13457 df-hash 14288 df-struct 17112 df-slot 17147 df-ndx 17159 df-base 17175 df-edgf 29076 df-vtx 29085 df-iedg 29086 df-edg 29135 df-uhgr 29145 df-upgr 29169 df-uspgr 29237 df-usgr 29238 df-nbgr 29420 df-clnbgr 48311 df-isubgr 48353 df-stgr 48444

This theorem is referenced by: isubgr3stgrlem8 48465

W3C validator