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 48361

Description: Lemma 7 for isubgr3stgr 48364. (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 48346	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦})))
3	1, 2	mp1i 13	. . 3 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦})))
4		c0ex 11140	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
5	4	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 0 ∈ V)
6		prssg 4777	. . . . . . . . . . . 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 6796	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶–1-1-onto→𝑊 → ^◡𝐹:𝑊–1-1-onto→𝐶)
9		f1ofn 6785	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹:𝑊–1-1-onto→𝐶 → ^◡𝐹 Fn 𝑊)
10		isubgr3stgr.w	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑊 = (Vtx‘𝑆)
11		isubgr3stgr.s	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = (StarGr‘𝑁)
12	11	fveq2i 6847	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Vtx‘𝑆) = (Vtx‘(StarGr‘𝑁))
13		stgrvtx 48343	. . . . . . . . . . . . . . . . . . . . 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 6600	. . . . . . . . . . . . . . . . . 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 6927	. . . . . . . . 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 48218	. . . . . . . . . . . . . . . . 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 7236	. . . . . . . . . . . . 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 6784	. . . . . . . . . . . . . . . . . 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 13553	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑁) ⊆ (0...𝑁)
49	48	sseli 3931	. . . . . . . . . . . . . . . . 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 7041	. . . . . . . . . . . . . 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 29276	. . . . . . . . . . . . . . . . . . . . . 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 48220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉
59	32, 58	eqsstri 3982	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐶 ⊆ 𝑉
60	59, 52	sselid 3933	. . . . . . . . . . . . . . . . . . . 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 48223	. . . . . . . . . . . . . . . . . 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 6783	. . . . . . . . . . . . . . . . . . . . . . . 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 13554	. . . . . . . . . . . . . . . . . . . . . . . . 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 7214	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((^◡𝐹:𝑊–1-1→𝐶 ∧ (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → 𝑦 = 0))
78	72, 76, 77	syl2an 597	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → 𝑦 = 0))
79		elfznn 13483	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
80		nnne0 12193	. . . . . . . . . . . . . . . . . . . . . . . 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 4691	. . . . . . . . . . . . . . . . . . . 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 4779	. . . . . . . . . . . . . . 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 4692	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹‘0) = 𝑋 → {(^◡𝐹‘0), (^◡𝐹‘𝑦)} = {𝑋, (^◡𝐹‘𝑦)})
101	100	eleq1d 2822	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘0) = 𝑋 → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ↔ {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
102	100	sseq1d 3967	. . . . . . . . . . . . . 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 29277	. . . . . . . . . . 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 48255	. . . . . . . . . 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 3961	. . . . . . 7 ⊢ (𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) ↔ {0, 𝑦} ⊆ (0...𝑁)))
119		imaeq2 6025	. . . . . . . 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 3442 ⊆ wss 3903 {cpr 4584 ↦ cmpt 5181 ^◡ccnv 5633 “ cima 5637 Fn wfn 6497 ⟶wf 6498 –1-1→wf1 6499 –1-1-onto→wf1o 6501 ‘cfv 6502 (class class class)co 7370 0cc0 11040 1c1 11041 ℕcn 12159 ℕ₀cn0 12415 ...cfz 13437 Vtxcvtx 29087 Edgcedg 29138 UHGraphcuhgr 29147 UPGraphcupgr 29171 USGraphcusgr 29240 NeighbVtx cnbgr 29423 ClNeighbVtx cclnbgr 48207 ISubGr cisubgr 48249 StarGrcstgr 48340

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 5226 ax-sep 5245 ax-nul 5255 ax-pow 5314 ax-pr 5381 ax-un 7692 ax-cnex 11096 ax-resscn 11097 ax-1cn 11098 ax-icn 11099 ax-addcl 11100 ax-addrcl 11101 ax-mulcl 11102 ax-mulrcl 11103 ax-mulcom 11104 ax-addass 11105 ax-mulass 11106 ax-distr 11107 ax-i2m1 11108 ax-1ne0 11109 ax-1rid 11110 ax-rnegex 11111 ax-rrecex 11112 ax-cnre 11113 ax-pre-lttri 11114 ax-pre-lttrn 11115 ax-pre-ltadd 11116 ax-pre-mulgt0 11117

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 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5529 df-eprel 5534 df-po 5542 df-so 5543 df-fr 5587 df-we 5589 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6269 df-ord 6330 df-on 6331 df-lim 6332 df-suc 6333 df-iota 6458 df-fun 6504 df-fn 6505 df-f 6506 df-f1 6507 df-fo 6508 df-f1o 6509 df-fv 6510 df-riota 7327 df-ov 7373 df-oprab 7374 df-mpo 7375 df-om 7821 df-1st 7945 df-2nd 7946 df-frecs 8235 df-wrecs 8266 df-recs 8315 df-rdg 8353 df-1o 8409 df-2o 8410 df-oadd 8413 df-er 8647 df-en 8898 df-dom 8899 df-sdom 8900 df-fin 8901 df-dju 9827 df-card 9865 df-pnf 11182 df-mnf 11183 df-xr 11184 df-ltxr 11185 df-le 11186 df-sub 11380 df-neg 11381 df-nn 12160 df-2 12222 df-3 12223 df-4 12224 df-5 12225 df-6 12226 df-7 12227 df-8 12228 df-9 12229 df-n0 12416 df-xnn0 12489 df-z 12503 df-dec 12622 df-uz 12766 df-fz 13438 df-hash 14268 df-struct 17088 df-slot 17123 df-ndx 17135 df-base 17151 df-edgf 29080 df-vtx 29089 df-iedg 29090 df-edg 29139 df-uhgr 29149 df-upgr 29173 df-uspgr 29241 df-usgr 29242 df-nbgr 29424 df-clnbgr 48208 df-isubgr 48250 df-stgr 48341

This theorem is referenced by: isubgr3stgrlem8 48362

W3C validator