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 47966

Description: Lemma 7 for isubgr3stgr 47969. (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 47951	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦})))
3	1, 2	mp1i 13	. . 3 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦})))
4		c0ex 11109	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
5	4	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 0 ∈ V)
6		prssg 4770	. . . . . . . . . . . 12 ⊢ ((0 ∈ V ∧ 𝑦 ∈ (1...𝑁)) → ((0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ {0, 𝑦} ⊆ (0...𝑁)))
7	5, 6	sylan 580	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ {0, 𝑦} ⊆ (0...𝑁)))
8		f1ocnv 6776	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶–1-1-onto→𝑊 → ^◡𝐹:𝑊–1-1-onto→𝐶)
9		f1ofn 6765	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹:𝑊–1-1-onto→𝐶 → ^◡𝐹 Fn 𝑊)
10		isubgr3stgr.w	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑊 = (Vtx‘𝑆)
11		isubgr3stgr.s	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = (StarGr‘𝑁)
12	11	fveq2i 6825	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Vtx‘𝑆) = (Vtx‘(StarGr‘𝑁))
13		stgrvtx 47948	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → (Vtx‘(StarGr‘𝑁)) = (0...𝑁))
14	1, 13	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Vtx‘(StarGr‘𝑁)) = (0...𝑁)
15	10, 12, 14	3eqtri 2756	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑊 = (0...𝑁)
16	15	fneq2i 6580	. . . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ^◡𝐹 Fn (0...𝑁))
20	19	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ^◡𝐹 Fn (0...𝑁))
21	20	anim1i 615	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))) → (^◡𝐹 Fn (0...𝑁) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))))
22		3anass 1094	. . . . . . . . . . . . 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 6906	. . . . . . . . 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 47823	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
31	30	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
32		isubgr3stgr.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)
33	31, 32	eleqtrrdi 2839	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝐶)
34		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) → 𝐹:𝐶–1-1-onto→𝑊)
35	33, 34	anim12ci 614	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐹:𝐶–1-1-onto→𝑊 ∧ 𝑋 ∈ 𝐶))
36		simprr 772	. . . . . . . . . . . . . 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 7215	. . . . . . . . . . . . 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 2839	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝐶)
43	42	ad3antlr 731	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑋 ∈ 𝐶)
44		f1of 6764	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹:𝑊–1-1-onto→𝐶 → ^◡𝐹:𝑊⟶𝐶)
45	8, 44	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶–1-1-onto→𝑊 → ^◡𝐹:𝑊⟶𝐶)
46	45	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ^◡𝐹:𝑊⟶𝐶)
47	46	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ^◡𝐹:𝑊⟶𝐶)
48		fz1ssfz0 13526	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑁) ⊆ (0...𝑁)
49	48	sseli 3931	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ (0...𝑁))
50	49, 15	eleqtrrdi 2839	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ 𝑊)
51	50	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑦 ∈ 𝑊)
52	47, 51	ffvelcdmd 7019	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (^◡𝐹‘𝑦) ∈ 𝐶)
53	43, 52	jca 511	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶))
54	32	eleq2i 2820	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝐹‘𝑦) ∈ 𝐶 ↔ (^◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋))
55		usgrupgr 29130	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph)
56	55	anim1i 615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉))
57	56	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉))
58	29	clnbgrssvtx 47825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉
59	32, 58	eqsstri 3982	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐶 ⊆ 𝑉
60	59, 52	sselid 3933	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (^◡𝐹‘𝑦) ∈ 𝑉)
61		df-3an 1088	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉) ↔ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉) ∧ (^◡𝐹‘𝑦) ∈ 𝑉))
62	57, 60, 61	sylanbrc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉))
63	62	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉))
64		isubgr3stgr.e	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐸 = (Edg‘𝐺)
65	29, 64	clnbupgrel 47828	. . . . . . . . . . . . . . . . . 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 2741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((^◡𝐹‘0) = 𝑋 → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) ↔ (^◡𝐹‘𝑦) = 𝑋))
69	68	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) ↔ (^◡𝐹‘𝑦) = 𝑋))
70		f1of1 6763	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (^◡𝐹:𝑊–1-1-onto→𝐶 → ^◡𝐹:𝑊–1-1→𝐶)
71	8, 70	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐶–1-1-onto→𝑊 → ^◡𝐹:𝑊–1-1→𝐶)
72	71	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → ^◡𝐹:𝑊–1-1→𝐶)
73		0elfz 13527	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ₀ → 0 ∈ (0...𝑁))
74	1, 73	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ (0...𝑁)
75	74, 15	eleqtrri 2827	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ 𝑊
76	50, 75	jctir 520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑁) → (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊))
77		f1veqaeq 7193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((^◡𝐹:𝑊–1-1→𝐶 ∧ (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → 𝑦 = 0))
78	72, 76, 77	syl2an 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → 𝑦 = 0))
79		elfznn 13456	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
80		nnne0 12162	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0)
81		eqneqall 2936	. . . . . . . . . . . . . . . . . . . . . . . 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 4684	. . . . . . . . . . . . . . . . . . . 20 ⊢ {(^◡𝐹‘𝑦), 𝑋} = {𝑋, (^◡𝐹‘𝑦)}
90	89	eleq1i 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸 ↔ {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸)
91	90	biimpi 216	. . . . . . . . . . . . . . . . . 18 ⊢ ({(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸)
92	91	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ({(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
93	88, 92	jaod 859	. . . . . . . . . . . . . . . 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 4772	. . . . . . . . . . . . . . 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 689	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ({𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶))
100		preq1 4685	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹‘0) = 𝑋 → {(^◡𝐹‘0), (^◡𝐹‘𝑦)} = {𝑋, (^◡𝐹‘𝑦)})
101	100	eleq1d 2813	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘0) = 𝑋 → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ↔ {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
102	100	sseq1d 3967	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘0) = 𝑋 → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶 ↔ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶))
103	101, 102	anbi12d 632	. . . . . . . . . . . . 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 687	. . . . . . . . . 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 29131	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
109	108	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝐺 ∈ UHGraph)
110	59	a1i 11	. . . . . . . . . 10 ⊢ ({0, 𝑦} ⊆ (0...𝑁) → 𝐶 ⊆ 𝑉)
111		eqid 2729	. . . . . . . . . . 11 ⊢ (𝐺 ISubGr 𝐶) = (𝐺 ISubGr 𝐶)
112		isubgr3stgr.i	. . . . . . . . . . 11 ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))
113	29, 64, 111, 112	isubgredg 47860	. . . . . . . . . 10 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐶 ⊆ 𝑉) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐼 ↔ ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶)))
114	109, 110, 113	syl2an 596	. . . . . . . . 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 2828	. . . . . . 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 6007	. . . . . . . 8 ⊢ (𝐽 = {0, 𝑦} → (^◡𝐹 “ 𝐽) = (^◡𝐹 “ {0, 𝑦}))
120	119	eleq1d 2813	. . . . . . 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 3130	. . . 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 1117	1 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (^◡𝐹 “ 𝐽) ∈ 𝐼)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∃wrex 3053 Vcvv 3436 ⊆ wss 3903 {cpr 4579 ↦ cmpt 5173 ^◡ccnv 5618 “ cima 5622 Fn wfn 6477 ⟶wf 6478 –1-1→wf1 6479 –1-1-onto→wf1o 6481 ‘cfv 6482 (class class class)co 7349 0cc0 11009 1c1 11010 ℕcn 12128 ℕ₀cn0 12384 ...cfz 13410 Vtxcvtx 28941 Edgcedg 28992 UHGraphcuhgr 29001 UPGraphcupgr 29025 USGraphcusgr 29094 NeighbVtx cnbgr 29277 ClNeighbVtx cclnbgr 47812 ISubGr cisubgr 47854 StarGrcstgr 47945

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-oadd 8392 df-er 8625 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-dju 9797 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-5 12194 df-6 12195 df-7 12196 df-8 12197 df-9 12198 df-n0 12385 df-xnn0 12458 df-z 12472 df-dec 12592 df-uz 12736 df-fz 13411 df-hash 14238 df-struct 17058 df-slot 17093 df-ndx 17105 df-base 17121 df-edgf 28934 df-vtx 28943 df-iedg 28944 df-edg 28993 df-uhgr 29003 df-upgr 29027 df-uspgr 29095 df-usgr 29096 df-nbgr 29278 df-clnbgr 47813 df-isubgr 47855 df-stgr 47946

This theorem is referenced by: isubgr3stgrlem8 47967

W3C validator