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 47975

Description: Lemma 7 for isubgr3stgr 47978. (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 47960	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦})))
3	1, 2	mp1i 13	. . 3 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦})))
4		c0ex 11175	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
5	4	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) → 0 ∈ V)
6		prssg 4786	. . . . . . . . . . . 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 6815	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶–1-1-onto→𝑊 → ^◡𝐹:𝑊–1-1-onto→𝐶)
9		f1ofn 6804	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹:𝑊–1-1-onto→𝐶 → ^◡𝐹 Fn 𝑊)
10		isubgr3stgr.w	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑊 = (Vtx‘𝑆)
11		isubgr3stgr.s	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = (StarGr‘𝑁)
12	11	fveq2i 6864	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Vtx‘𝑆) = (Vtx‘(StarGr‘𝑁))
13		stgrvtx 47957	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → (Vtx‘(StarGr‘𝑁)) = (0...𝑁))
14	1, 13	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Vtx‘(StarGr‘𝑁)) = (0...𝑁)
15	10, 12, 14	3eqtri 2757	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑊 = (0...𝑁)
16	15	fneq2i 6619	. . . . . . . . . . . . . . . . . 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 6947	. . . . . . . . 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 47834	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
31	30	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
32		isubgr3stgr.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)
33	31, 32	eleqtrrdi 2840	. . . . . . . . . . . . . . 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 7256	. . . . . . . . . . . . 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 2840	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝐶)
43	42	ad3antlr 731	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑋 ∈ 𝐶)
44		f1of 6803	. . . . . . . . . . . . . . . . . 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 13591	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑁) ⊆ (0...𝑁)
49	48	sseli 3945	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ (0...𝑁))
50	49, 15	eleqtrrdi 2840	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ 𝑊)
51	50	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑦 ∈ 𝑊)
52	47, 51	ffvelcdmd 7060	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (^◡𝐹‘𝑦) ∈ 𝐶)
53	43, 52	jca 511	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶))
54	32	eleq2i 2821	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝐹‘𝑦) ∈ 𝐶 ↔ (^◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋))
55		usgrupgr 29119	. . . . . . . . . . . . . . . . . . . . . 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 47836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉
59	32, 58	eqsstri 3996	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐶 ⊆ 𝑉
60	59, 52	sselid 3947	. . . . . . . . . . . . . . . . . . . 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 47839	. . . . . . . . . . . . . . . . . 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 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((^◡𝐹‘0) = 𝑋 → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) ↔ (^◡𝐹‘𝑦) = 𝑋))
69	68	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) ↔ (^◡𝐹‘𝑦) = 𝑋))
70		f1of1 6802	. . . . . . . . . . . . . . . . . . . . . . . 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 13592	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ₀ → 0 ∈ (0...𝑁))
74	1, 73	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ (0...𝑁)
75	74, 15	eleqtrri 2828	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ 𝑊
76	50, 75	jctir 520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑁) → (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊))
77		f1veqaeq 7234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((^◡𝐹:𝑊–1-1→𝐶 ∧ (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → 𝑦 = 0))
78	72, 76, 77	syl2an 596	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → 𝑦 = 0))
79		elfznn 13521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
80		nnne0 12227	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0)
81		eqneqall 2937	. . . . . . . . . . . . . . . . . . . . . . . 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 4699	. . . . . . . . . . . . . . . . . . . 20 ⊢ {(^◡𝐹‘𝑦), 𝑋} = {𝑋, (^◡𝐹‘𝑦)}
90	89	eleq1i 2820	. . . . . . . . . . . . . . . . . . 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 4788	. . . . . . . . . . . . . . 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 4700	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹‘0) = 𝑋 → {(^◡𝐹‘0), (^◡𝐹‘𝑦)} = {𝑋, (^◡𝐹‘𝑦)})
101	100	eleq1d 2814	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘0) = 𝑋 → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ↔ {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
102	100	sseq1d 3981	. . . . . . . . . . . . . 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 29120	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
109	108	ad3antrrr 730	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶–1-1-onto→𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝐺 ∈ UHGraph)
110	59	a1i 11	. . . . . . . . . 10 ⊢ ({0, 𝑦} ⊆ (0...𝑁) → 𝐶 ⊆ 𝑉)
111		eqid 2730	. . . . . . . . . . 11 ⊢ (𝐺 ISubGr 𝐶) = (𝐺 ISubGr 𝐶)
112		isubgr3stgr.i	. . . . . . . . . . 11 ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))
113	29, 64, 111, 112	isubgredg 47870	. . . . . . . . . 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 2829	. . . . . . 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 3975	. . . . . . 7 ⊢ (𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) ↔ {0, 𝑦} ⊆ (0...𝑁)))
119		imaeq2 6030	. . . . . . . 8 ⊢ (𝐽 = {0, 𝑦} → (^◡𝐹 “ 𝐽) = (^◡𝐹 “ {0, 𝑦}))
120	119	eleq1d 2814	. . . . . . 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 3135	. . . 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 2926 ∃wrex 3054 Vcvv 3450 ⊆ wss 3917 {cpr 4594 ↦ cmpt 5191 ^◡ccnv 5640 “ cima 5644 Fn wfn 6509 ⟶wf 6510 –1-1→wf1 6511 –1-1-onto→wf1o 6513 ‘cfv 6514 (class class class)co 7390 0cc0 11075 1c1 11076 ℕcn 12193 ℕ₀cn0 12449 ...cfz 13475 Vtxcvtx 28930 Edgcedg 28981 UHGraphcuhgr 28990 UPGraphcupgr 29014 USGraphcusgr 29083 NeighbVtx cnbgr 29266 ClNeighbVtx cclnbgr 47823 ISubGr cisubgr 47864 StarGrcstgr 47954

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 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152

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 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7846 df-1st 7971 df-2nd 7972 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-er 8674 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-dju 9861 df-card 9899 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-nn 12194 df-2 12256 df-3 12257 df-4 12258 df-5 12259 df-6 12260 df-7 12261 df-8 12262 df-9 12263 df-n0 12450 df-xnn0 12523 df-z 12537 df-dec 12657 df-uz 12801 df-fz 13476 df-hash 14303 df-struct 17124 df-slot 17159 df-ndx 17171 df-base 17187 df-edgf 28923 df-vtx 28932 df-iedg 28933 df-edg 28982 df-uhgr 28992 df-upgr 29016 df-uspgr 29084 df-usgr 29085 df-nbgr 29267 df-clnbgr 47824 df-isubgr 47865 df-stgr 47955

This theorem is referenced by: isubgr3stgrlem8 47976

W3C validator