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 49273

Description: Lemma 7 for isubgr3stgr 49276. (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-1onto𝑊 ∧ (𝐹‘𝑋) = 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 49258	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦})))
3	1, 2	mp1i 14	. . 3 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) ↔ (𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦})))
4		c0ex 11324	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
5	4	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → 0 ∈ V)
6		prssg 4778	. . . . . . . . . . . 12 ⊢ ((0 ∈ V ∧ 𝑦 ∈ (1...𝑁)) → ((0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ {0, 𝑦} ⊆ (0...𝑁)))
7	5, 6	sylan 592	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ {0, 𝑦} ⊆ (0...𝑁)))
8		f1ocnv 6856	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶⟶1-1onto𝑊 → ^◡𝐹:𝑊⟶1-1onto𝐶)
9		f1ofn 6844	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹:𝑊⟶1-1onto𝐶 → ^◡𝐹 Fn 𝑊)
10		isubgr3stgr.w	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑊 = (Vtx‘𝑆)
11		isubgr3stgr.s	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑆 = (StarGr‘𝑁)
12	11	fveq2i 6908	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Vtx‘𝑆) = (Vtx‘(StarGr‘𝑁))
13		stgrvtx 49255	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑁 ∈ ℕ₀ → (Vtx‘(StarGr‘𝑁)) = (0...𝑁))
14	1, 13	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Vtx‘(StarGr‘𝑁)) = (0...𝑁)
15	10, 12, 14	3eqtri 2790	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑊 = (0...𝑁)
16	15	fneq2i 6656	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹 Fn 𝑊 ↔ ^◡𝐹 Fn (0...𝑁))
17	9, 16	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ (^◡𝐹:𝑊⟶1-1onto𝐶 → ^◡𝐹 Fn (0...𝑁))
18	8, 17	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝐹:𝐶⟶1-1onto𝑊 → ^◡𝐹 Fn (0...𝑁))
19	18	ad2antrl 741	. . . . . . . . . . . . . . 15 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → ^◡𝐹 Fn (0...𝑁))
20	19	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ^◡𝐹 Fn (0...𝑁))
21	20	anim1i 627	. . . . . . . . . . . . 13 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))) → (^◡𝐹 Fn (0...𝑁) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))))
22		3anass 1111	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) ↔ (^◡𝐹 Fn (0...𝑁) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))))
23	21, 22	sylibr 237	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))) → (^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)))
24	23	ex 418	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) → (^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))))
25	7, 24	sylbird 263	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ({0, 𝑦} ⊆ (0...𝑁) → (^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁))))
26	25	imp 412	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → (^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)))
27		fnimapr 6988	. . . . . . . . 9 ⊢ ((^◡𝐹 Fn (0...𝑁) ∧ 0 ∈ (0...𝑁) ∧ 𝑦 ∈ (0...𝑁)) → (^◡𝐹 “ {0, 𝑦}) = {(^◡𝐹‘0), (^◡𝐹‘𝑦)})
28	26, 27	syl 18	. . . . . . . 8 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → (^◡𝐹 “ {0, 𝑦}) = {(^◡𝐹‘0), (^◡𝐹‘𝑦)})
29		isubgr3stgr.v	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑉 = (Vtx‘𝐺)
30	29	clnbgrvtxel 49130	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
31	30	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ (𝐺 ClNeighbVtx 𝑋))
32		isubgr3stgr.c	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 = (𝐺 ClNeighbVtx 𝑋)
33	31, 32	eleqtrrdi 2875	. . . . . . . . . . . . . . 15 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝐶)
34		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0) → 𝐹:𝐶⟶1-1onto𝑊)
35	33, 34	anim12ci 626	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐹:𝐶⟶1-1onto𝑊 ∧ 𝑋 ∈ 𝐶))
36		simprr 785	. . . . . . . . . . . . . 14 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐹‘𝑋) = 0)
37	35, 36	jca 521	. . . . . . . . . . . . 13 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → ((𝐹:𝐶⟶1-1onto𝑊 ∧ 𝑋 ∈ 𝐶) ∧ (𝐹‘𝑋) = 0))
38	37	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((𝐹:𝐶⟶1-1onto𝑊 ∧ 𝑋 ∈ 𝐶) ∧ (𝐹‘𝑋) = 0))
39		f1ocnvfv 7306	. . . . . . . . . . . . 13 ⊢ ((𝐹:𝐶⟶1-1onto𝑊 ∧ 𝑋 ∈ 𝐶) → ((𝐹‘𝑋) = 0 → (^◡𝐹‘0) = 𝑋))
40	39	imp 412	. . . . . . . . . . . 12 ⊢ (((𝐹:𝐶⟶1-1onto𝑊 ∧ 𝑋 ∈ 𝐶) ∧ (𝐹‘𝑋) = 0) → (^◡𝐹‘0) = 𝑋)
41	38, 40	syl 18	. . . . . . . . . . 11 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (^◡𝐹‘0) = 𝑋)
42	30, 32	eleqtrrdi 2875	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝐶)
43	42	ad3antlr 744	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑋 ∈ 𝐶)
44		f1of 6843	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡𝐹:𝑊⟶1-1onto𝐶 → ^◡𝐹:𝑊⟶𝐶)
45	8, 44	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹:𝐶⟶1-1onto𝑊 → ^◡𝐹:𝑊⟶𝐶)
46	45	ad2antrl 741	. . . . . . . . . . . . . . . 16 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → ^◡𝐹:𝑊⟶𝐶)
47	46	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ^◡𝐹:𝑊⟶𝐶)
48		fz1ssfz0 13781	. . . . . . . . . . . . . . . . . 18 ⊢ (1...𝑁) ⊆ (0...𝑁)
49	48	sseli 3909	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ (0...𝑁))
50	49, 15	eleqtrrdi 2875	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ 𝑊)
51	50	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝑦 ∈ 𝑊)
52	47, 51	ffvelcdmd 7106	. . . . . . . . . . . . . 14 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (^◡𝐹‘𝑦) ∈ 𝐶)
53	43, 52	jca 521	. . . . . . . . . . . . 13 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶))
54	32	eleq2i 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((^◡𝐹‘𝑦) ∈ 𝐶 ↔ (^◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋))
55		usgrupgr 29793	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UPGraph)
56	55	anim1i 627	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉))
57	56	ad2antrr 739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉))
58	29	clnbgrssvtx 49132	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐺 ClNeighbVtx 𝑋) ⊆ 𝑉
59	32, 58	eqsstri 3959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐶 ⊆ 𝑉
60	59, 52	sselid 3911	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (^◡𝐹‘𝑦) ∈ 𝑉)
61		df-3an 1105	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉) ↔ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉) ∧ (^◡𝐹‘𝑦) ∈ 𝑉))
62	57, 60, 61	sylanbrc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉))
63	62	ad2antrr 739	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → (𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉))
64		isubgr3stgr.e	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐸 = (Edg‘𝐺)
65	29, 64	clnbupgrel 49135	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐺 ∈ UPGraph ∧ 𝑋 ∈ 𝑉 ∧ (^◡𝐹‘𝑦) ∈ 𝑉) → ((^◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((^◡𝐹‘𝑦) = 𝑋 ∨ {(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸)))
66	63, 65	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((^◡𝐹‘𝑦) ∈ (𝐺 ClNeighbVtx 𝑋) ↔ ((^◡𝐹‘𝑦) = 𝑋 ∨ {(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸)))
67	54, 66	bitrid 286	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((^◡𝐹‘𝑦) ∈ 𝐶 ↔ ((^◡𝐹‘𝑦) = 𝑋 ∨ {(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸)))
68		eqeq2 2775	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((^◡𝐹‘0) = 𝑋 → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) ↔ (^◡𝐹‘𝑦) = 𝑋))
69	68	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) ↔ (^◡𝐹‘𝑦) = 𝑋))
70		f1of1 6842	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (^◡𝐹:𝑊⟶1-1onto𝐶 → ^◡𝐹:𝑊⟶1-1𝐶)
71	8, 70	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐹:𝐶⟶1-1onto𝑊 → ^◡𝐹:𝑊⟶1-1𝐶)
72	71	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → ^◡𝐹:𝑊⟶1-1𝐶)
73		0elfz 13782	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑁 ∈ ℕ₀ → 0 ∈ (0...𝑁))
74	1, 73	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ (0...𝑁)
75	74, 15	eleqtrri 2863	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 0 ∈ 𝑊
76	50, 75	jctir 530	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑁) → (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊))
77		f1veqaeq 7280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((^◡𝐹:𝑊⟶1-1𝐶 ∧ (𝑦 ∈ 𝑊 ∧ 0 ∈ 𝑊)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → 𝑦 = 0))
78	72, 76, 77	syl2an 608	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → 𝑦 = 0))
79		elfznn 13711	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
80		nnne0 12396	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ ℕ → 𝑦 ≠ 0)
81		eqneqall 2970	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 0 → (𝑦 ≠ 0 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
82	80, 81	syl5com 32	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ ℕ → (𝑦 = 0 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
83	79, 82	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (1...𝑁) → (𝑦 = 0 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
84	83	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝑦 = 0 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
85	78, 84	syld 48	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
86	85	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ((^◡𝐹‘𝑦) = (^◡𝐹‘0) → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
87	69, 86	sylbird 263	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ((^◡𝐹‘𝑦) = 𝑋 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
88	87	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((^◡𝐹‘𝑦) = 𝑋 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
89		prcom 4693	. . . . . . . . . . . . . . . . . . . 20 ⊢ {(^◡𝐹‘𝑦), 𝑋} = {𝑋, (^◡𝐹‘𝑦)}
90	89	eleq1i 2855	. . . . . . . . . . . . . . . . . . 19 ⊢ ({(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸 ↔ {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸)
91	90	biimpi 219	. . . . . . . . . . . . . . . . . 18 ⊢ ({(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸)
92	91	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ({(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
93	88, 92	jaod 873	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → (((^◡𝐹‘𝑦) = 𝑋 ∨ {(^◡𝐹‘𝑦), 𝑋} ∈ 𝐸) → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
94	67, 93	sylbid 243	. . . . . . . . . . . . . . 15 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ 𝑋 ∈ 𝐶) → ((^◡𝐹‘𝑦) ∈ 𝐶 → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
95	94	impr 460	. . . . . . . . . . . . . 14 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ (𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶)) → {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸)
96		prssi 4780	. . . . . . . . . . . . . . 15 ⊢ ((𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶) → {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶)
97	96	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ (𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶)) → {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶)
98	95, 97	jca 521	. . . . . . . . . . . . 13 ⊢ ((((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) ∧ (𝑋 ∈ 𝐶 ∧ (^◡𝐹‘𝑦) ∈ 𝐶)) → ({𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶))
99	53, 98	mpidan 702	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ({𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶))
100		preq1 4694	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹‘0) = 𝑋 → {(^◡𝐹‘0), (^◡𝐹‘𝑦)} = {𝑋, (^◡𝐹‘𝑦)})
101	100	eleq1d 2849	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘0) = 𝑋 → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ↔ {𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸))
102	100	sseq1d 3944	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹‘0) = 𝑋 → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶 ↔ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶))
103	101, 102	anbi12d 644	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹‘0) = 𝑋 → (({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶) ↔ ({𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶)))
104	103	adantl 487	. . . . . . . . . . . 12 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → (({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶) ↔ ({𝑋, (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {𝑋, (^◡𝐹‘𝑦)} ⊆ 𝐶)))
105	99, 104	mpbird 260	. . . . . . . . . . 11 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ (^◡𝐹‘0) = 𝑋) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶))
106	41, 105	mpdan 700	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶))
107	106	adantr 486	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶))
108		usgruhgr 29794	. . . . . . . . . . 11 ⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph)
109	108	ad3antrrr 743	. . . . . . . . . 10 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → 𝐺 ∈ UHGraph)
110	59	a1i 11	. . . . . . . . . 10 ⊢ ({0, 𝑦} ⊆ (0...𝑁) → 𝐶 ⊆ 𝑉)
111		eqid 2763	. . . . . . . . . . 11 ⊢ (𝐺 ISubGr 𝐶) = (𝐺 ISubGr 𝐶)
112		isubgr3stgr.i	. . . . . . . . . . 11 ⊢ 𝐼 = (Edg‘(𝐺 ISubGr 𝐶))
113	29, 64, 111, 112	isubgredg 49167	. . . . . . . . . 10 ⊢ ((𝐺 ∈ UHGraph ∧ 𝐶 ⊆ 𝑉) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐼 ↔ ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶)))
114	109, 110, 113	syl2an 608	. . . . . . . . 9 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐼 ↔ ({(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐸 ∧ {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ⊆ 𝐶)))
115	107, 114	mpbird 260	. . . . . . . 8 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → {(^◡𝐹‘0), (^◡𝐹‘𝑦)} ∈ 𝐼)
116	28, 115	eqeltrd 2864	. . . . . . 7 ⊢ (((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) ∧ {0, 𝑦} ⊆ (0...𝑁)) → (^◡𝐹 “ {0, 𝑦}) ∈ 𝐼)
117	116	ex 418	. . . . . 6 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → ({0, 𝑦} ⊆ (0...𝑁) → (^◡𝐹 “ {0, 𝑦}) ∈ 𝐼))
118		sseq1 3938	. . . . . . 7 ⊢ (𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) ↔ {0, 𝑦} ⊆ (0...𝑁)))
119		imaeq2 6059	. . . . . . . 8 ⊢ (𝐽 = {0, 𝑦} → (^◡𝐹 “ 𝐽) = (^◡𝐹 “ {0, 𝑦}))
120	119	eleq1d 2849	. . . . . . 7 ⊢ (𝐽 = {0, 𝑦} → ((^◡𝐹 “ 𝐽) ∈ 𝐼 ↔ (^◡𝐹 “ {0, 𝑦}) ∈ 𝐼))
121	118, 120	imbi12d 347	. . . . . 6 ⊢ (𝐽 = {0, 𝑦} → ((𝐽 ⊆ (0...𝑁) → (^◡𝐹 “ 𝐽) ∈ 𝐼) ↔ ({0, 𝑦} ⊆ (0...𝑁) → (^◡𝐹 “ {0, 𝑦}) ∈ 𝐼)))
122	117, 121	syl5ibrcom 250	. . . . 5 ⊢ ((((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) ∧ 𝑦 ∈ (1...𝑁)) → (𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) → (^◡𝐹 “ 𝐽) ∈ 𝐼)))
123	122	rexlimdva 3167	. . . 4 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → (∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦} → (𝐽 ⊆ (0...𝑁) → (^◡𝐹 “ 𝐽) ∈ 𝐼)))
124	123	impcomd 417	. . 3 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → ((𝐽 ⊆ (0...𝑁) ∧ ∃𝑦 ∈ (1...𝑁)𝐽 = {0, 𝑦}) → (^◡𝐹 “ 𝐽) ∈ 𝐼))
125	3, 124	sylbid 243	. 2 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0)) → (𝐽 ∈ (Edg‘(StarGr‘𝑁)) → (^◡𝐹 “ 𝐽) ∈ 𝐼))
126	125	3impia 1135	1 ⊢ (((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉) ∧ (𝐹:𝐶⟶1-1onto𝑊 ∧ (𝐹‘𝑋) = 0) ∧ 𝐽 ∈ (Edg‘(StarGr‘𝑁))) → (^◡𝐹 “ 𝐽) ∈ 𝐼)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 {cpr 4590 ↦ cmpt 5189 ^◡ccnv 5654 “ cima 5658 Fn wfn 6550 ⟶wf 6551 ⟶1-1wf1 6552 ⟶1-1ontowf1o 6554 ‘cfv 6555 (class class class)co 7440 0cc0 11224 1c1 11225 ℕcn 12359 ℕ₀cn0 12630 ...cfz 13663 Vtxcvtx 29601 Edgcedg 29652 UHGraphcuhgr 29661 UPGraphcupgr 29685 USGraphcusgr 29757 NeighbVtx cnbgr 29940 ClNeighbVtx cclnbgr 49119 ISubGr cisubgr 49161 StarGrcstgr 49252

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-om 7899 df-1st 8022 df-2nd 8023 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-2o 8502 df-oadd 8505 df-er 8742 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-dju 10006 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-nn 12360 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-7 12434 df-8 12435 df-9 12436 df-n0 12631 df-xnn0 12704 df-z 12718 df-dec 12839 df-uz 12990 df-fz 13664 df-hash 14499 df-struct 17351 df-slot 17386 df-ndx 17398 df-base 17414 df-edgf 29594 df-vtx 29603 df-iedg 29604 df-edg 29653 df-uhgr 29663 df-upgr 29687 df-uspgr 29758 df-usgr 29759 df-nbgr 29941 df-clnbgr 49120 df-isubgr 49162 df-stgr 49253

This theorem is used by: isubgr3stgrlem8 49274

W3C validator