1wlkres - Mathbox for Alexander van der Vekens

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

Theorem 1wlkres 40879

Description: The restriction ⟨𝐻, 𝑄⟩ of a 1-walk ⟨𝐹, 𝑃⟩ to an initial segment of the 1-walk (of length 𝑁) forms a 1-walk on the subgraph 𝑆 consisting of the edges in the initial segment. Formerly proven directly for Eulerian paths, see eupthres 41383. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.)

**Hypotheses**
Ref	Expression
1wlkres.v	⊢ 𝑉 = (Vtx‘𝐺)
1wlkres.i	⊢ 𝐼 = (iEdg‘𝐺)
1wlkres.d	⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃)
1wlkres.n	⊢ (𝜑 → 𝑁 ∈ (0..^(#‘𝐹)))
1wlkres.s	⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)
1wlkres.e	⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
1wlkres.h	⊢ 𝐻 = (𝐹 ↾ (0..^𝑁))
1wlkres.q	⊢ 𝑄 = (𝑃 ↾ (0...𝑁))

**Assertion**
Ref	Expression
1wlkres	⊢ (𝜑 → 𝐻(1Walks‘𝑆)𝑄)

Proof of Theorem 1wlkres Dummy variables 𝑘 𝑖 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1wlkres.h	. . 3 ⊢ 𝐻 = (𝐹 ↾ (0..^𝑁))
2		1wlkres.d	. . . . . . . 8 ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃)
3		1wlkres.i	. . . . . . . . 9 ⊢ 𝐼 = (iEdg‘𝐺)
4	3	1wlkf 40819	. . . . . . . 8 ⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
5		wrdfn 13174	. . . . . . . 8 ⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹 Fn (0..^(#‘𝐹)))
6	2, 4, 5	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐹 Fn (0..^(#‘𝐹)))
7		1wlkres.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0..^(#‘𝐹)))
8		elfzouz2 12353	. . . . . . . 8 ⊢ (𝑁 ∈ (0..^(#‘𝐹)) → (#‘𝐹) ∈ (ℤ_≥‘𝑁))
9		fzoss2 12365	. . . . . . . 8 ⊢ ((#‘𝐹) ∈ (ℤ_≥‘𝑁) → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
10	7, 8, 9	3syl 18	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
11		fnssres 5918	. . . . . . 7 ⊢ ((𝐹 Fn (0..^(#‘𝐹)) ∧ (0..^𝑁) ⊆ (0..^(#‘𝐹))) → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
12	6, 10, 11	syl2anc 691	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
13		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
14		fveq2 6103	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑥 → (𝐹‘𝑖) = (𝐹‘𝑥))
15	14	eqeq1d 2612	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑥 → ((𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
16	15	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) ∧ 𝑖 = 𝑥) → ((𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
17		fvres 6117	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0..^𝑁) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹‘𝑥))
18	17	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹‘𝑥))
19	18	eqcomd 2616	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
20	13, 16, 19	rspcedvd 3289	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ∃𝑖 ∈ (0..^𝑁)(𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
21	6	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝐹 Fn (0..^(#‘𝐹)))
22	10	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ (0..^(#‘𝐹)))
23	21, 22	fvelimabd 6164	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)) ↔ ∃𝑖 ∈ (0..^𝑁)(𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
24	20, 23	mpbird 246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)))
25	2, 4	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
26		wrdf 13165	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐼)
27	10	sselda 3568	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(#‘𝐹)))
28		ffvelrn 6265	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹:(0..^(#‘𝐹))⟶dom 𝐼 ∧ 𝑥 ∈ (0..^(#‘𝐹))) → (𝐹‘𝑥) ∈ dom 𝐼)
29	28	expcom 450	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → (𝐹‘𝑥) ∈ dom 𝐼))
30	27, 29	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → (𝐹‘𝑥) ∈ dom 𝐼))
31	30	com12 32	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) ∈ dom 𝐼))
32	31	expd 451	. . . . . . . . . . . . . 14 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ dom 𝐼)))
33	26, 32	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ dom 𝐼)))
34	25, 33	mpcom 37	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ dom 𝐼))
35	34	imp 444	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) ∈ dom 𝐼)
36	18, 35	eqeltrd 2688	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom 𝐼)
37	24, 36	elind 3760	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼))
38		dmres 5339	. . . . . . . . 9 ⊢ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼)
39	37, 38	syl6eleqr 2699	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
40		1wlkres.e	. . . . . . . . . . 11 ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
41	40	dmeqd 5248	. . . . . . . . . 10 ⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
42	41	eleq2d 2673	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
43	42	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
44	39, 43	mpbird 246	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
45	44	ralrimiva 2949	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
46		ffnfv 6295	. . . . . 6 ⊢ ((𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁) ∧ ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆)))
47	12, 45, 46	sylanbrc 695	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆))
48		fzossfz 12357	. . . . . . . . 9 ⊢ (0..^(#‘𝐹)) ⊆ (0...(#‘𝐹))
49	48, 7	sseldi 3566	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0...(#‘𝐹)))
50		1wlkreslem0 40877	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ (0...(#‘𝐹))) → (#‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
51	25, 49, 50	syl2anc 691	. . . . . . 7 ⊢ (𝜑 → (#‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
52	51	oveq2d 6565	. . . . . 6 ⊢ (𝜑 → (0..^(#‘(𝐹 ↾ (0..^𝑁)))) = (0..^𝑁))
53	52	feq2d 5944	. . . . 5 ⊢ (𝜑 → ((𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆)))
54	47, 53	mpbird 246	. . . 4 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
55		iswrdb 13166	. . . 4 ⊢ ((𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^(#‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
56	54, 55	sylibr 223	. . 3 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆))
57	1, 56	syl5eqel 2692	. 2 ⊢ (𝜑 → 𝐻 ∈ Word dom (iEdg‘𝑆))
58		1wlkres.v	. . . . . . . 8 ⊢ 𝑉 = (Vtx‘𝐺)
59	58	1wlkp 40821	. . . . . . 7 ⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉)
60	2, 59	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶𝑉)
61		1wlkres.s	. . . . . . 7 ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)
62	61	feq3d 5945	. . . . . 6 ⊢ (𝜑 → (𝑃:(0...(#‘𝐹))⟶(Vtx‘𝑆) ↔ 𝑃:(0...(#‘𝐹))⟶𝑉))
63	60, 62	mpbird 246	. . . . 5 ⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶(Vtx‘𝑆))
64		elfzuz3 12210	. . . . . 6 ⊢ (𝑁 ∈ (0...(#‘𝐹)) → (#‘𝐹) ∈ (ℤ_≥‘𝑁))
65		fzss2 12252	. . . . . 6 ⊢ ((#‘𝐹) ∈ (ℤ_≥‘𝑁) → (0...𝑁) ⊆ (0...(#‘𝐹)))
66	49, 64, 65	3syl 18	. . . . 5 ⊢ (𝜑 → (0...𝑁) ⊆ (0...(#‘𝐹)))
67	63, 66	fssresd 5984	. . . 4 ⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆))
68	1	fveq2i 6106	. . . . . . 7 ⊢ (#‘𝐻) = (#‘(𝐹 ↾ (0..^𝑁)))
69	68, 51	syl5eq 2656	. . . . . 6 ⊢ (𝜑 → (#‘𝐻) = 𝑁)
70	69	oveq2d 6565	. . . . 5 ⊢ (𝜑 → (0...(#‘𝐻)) = (0...𝑁))
71	70	feq2d 5944	. . . 4 ⊢ (𝜑 → ((𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆)))
72	67, 71	mpbird 246	. . 3 ⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆))
73		1wlkres.q	. . . 4 ⊢ 𝑄 = (𝑃 ↾ (0...𝑁))
74	73	feq1i 5949	. . 3 ⊢ (𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...(#‘𝐻))⟶(Vtx‘𝑆))
75	72, 74	sylibr 223	. 2 ⊢ (𝜑 → 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆))
76		wlkv 40815	. . . . . . 7 ⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
77	58, 3	is1wlk 40813	. . . . . . . 8 ⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
78	77	biimpd 218	. . . . . . 7 ⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(1Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
79	76, 78	mpcom 37	. . . . . 6 ⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
80	2, 79	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
81	80	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
82	69	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(#‘𝐻)) = (0..^𝑁))
83	82	eleq2d 2673	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) ↔ 𝑥 ∈ (0..^𝑁)))
84	73	fveq1i 6104	. . . . . . . . . . . . 13 ⊢ (𝑄‘𝑥) = ((𝑃 ↾ (0...𝑁))‘𝑥)
85		fzossfz 12357	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝑁) ⊆ (0...𝑁)
86	85	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0..^𝑁) ⊆ (0...𝑁))
87	86	sselda 3568	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0...𝑁))
88	87	fvresd 6118	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘𝑥) = (𝑃‘𝑥))
89	84, 88	syl5req 2657	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘𝑥) = (𝑄‘𝑥))
90	73	fveq1i 6104	. . . . . . . . . . . . 13 ⊢ (𝑄‘(𝑥 + 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1))
91		fzofzp1 12431	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁))
92	91	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁))
93	92	fvresd 6118	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) = (𝑃‘(𝑥 + 1)))
94	90, 93	syl5req 2657	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))
95	89, 94	jca 553	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
96	95	ex 449	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
97	83, 96	sylbid 229	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
98	97	imp 444	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
99	25	ancli 572	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝜑 ∧ 𝐹 ∈ Word dom 𝐼))
100	26	ffund 5962	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Word dom 𝐼 → Fun 𝐹)
101	100	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → Fun 𝐹)
102	101	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → Fun 𝐹)
103		fdm 5964	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:(0..^(#‘𝐹))⟶dom 𝐼 → dom 𝐹 = (0..^(#‘𝐹)))
104		sseq2 3590	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom 𝐹 = (0..^(#‘𝐹)) → ((0..^𝑁) ⊆ dom 𝐹 ↔ (0..^𝑁) ⊆ (0..^(#‘𝐹))))
105	10, 104	syl5ibr 235	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝐹 = (0..^(#‘𝐹)) → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
106	26, 103, 105	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
107	106	impcom 445	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → (0..^𝑁) ⊆ dom 𝐹)
108	107	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ dom 𝐹)
109		simpr 476	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
110	102, 108, 109	resfvresima 6398	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
111	99, 110	sylan 487	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
112	111	eqcomd 2616	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
113	112	ex 449	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
114	83, 113	sylbid 229	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^(#‘𝐻)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
115	114	imp 444	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
116	40	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
117	1	fveq1i 6104	. . . . . . . . . . 11 ⊢ (𝐻‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)
118	117	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐻‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
119	116, 118	fveq12d 6109	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → ((iEdg‘𝑆)‘(𝐻‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
120	115, 119	eqtr4d 2647	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥)))
121	98, 120	jca 553	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))))
122	7, 8	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (#‘𝐹) ∈ (ℤ_≥‘𝑁))
123	1	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻 = (𝐹 ↾ (0..^𝑁)))
124	123	fveq2d 6107	. . . . . . . . . . . . 13 ⊢ (𝜑 → (#‘𝐻) = (#‘(𝐹 ↾ (0..^𝑁))))
125	124, 51	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (𝜑 → (#‘𝐻) = 𝑁)
126	125	fveq2d 6107	. . . . . . . . . . 11 ⊢ (𝜑 → (ℤ_≥‘(#‘𝐻)) = (ℤ_≥‘𝑁))
127	122, 126	eleqtrrd 2691	. . . . . . . . . 10 ⊢ (𝜑 → (#‘𝐹) ∈ (ℤ_≥‘(#‘𝐻)))
128		fzoss2 12365	. . . . . . . . . 10 ⊢ ((#‘𝐹) ∈ (ℤ_≥‘(#‘𝐻)) → (0..^(#‘𝐻)) ⊆ (0..^(#‘𝐹)))
129	127, 128	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0..^(#‘𝐻)) ⊆ (0..^(#‘𝐹)))
130	129	sselda 3568	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → 𝑥 ∈ (0..^(#‘𝐹)))
131		1wlkslem1 40809	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)))))
132	131	rspcv 3278	. . . . . . . 8 ⊢ (𝑥 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)))))
133	130, 132	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)))))
134		eqeq12 2623	. . . . . . . . . 10 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1))))
135	134	adantr 480	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1))))
136		simpr 476	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥)))
137		sneq 4135	. . . . . . . . . . . 12 ⊢ ((𝑃‘𝑥) = (𝑄‘𝑥) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
138	137	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
139	138	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
140	136, 139	eqeq12d 2625	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)} ↔ ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}))
141		preq12 4214	. . . . . . . . . . 11 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))})
142	141	adantr 480	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))})
143	142, 136	sseq12d 3597	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ({(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)) ↔ {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
144	135, 140, 143	ifpbi123d 1021	. . . . . . . 8 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))) ↔ if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
145	144	biimpd 218	. . . . . . 7 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
146	121, 133, 145	sylsyld 59	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
147	146	com12 32	. . . . 5 ⊢ (∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
148	147	3ad2ant3 1077	. . . 4 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) → ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
149	81, 148	mpcom 37	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(#‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
150	149	ralrimiva 2949	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
151	58, 3, 2, 7, 61, 40, 1, 73	1wlkreslem 40878	. . 3 ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
152		eqid 2610	. . . 4 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
153		eqid 2610	. . . 4 ⊢ (iEdg‘𝑆) = (iEdg‘𝑆)
154	152, 153	is1wlk 40813	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(1Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))))
155	151, 154	syl 17	. 2 ⊢ (𝜑 → (𝐻(1Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(#‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))))
156	57, 75, 150, 155	mpbir3and 1238	1 ⊢ (𝜑 → 𝐻(1Walks‘𝑆)𝑄)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 if-wif 1006 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 Vcvv 3173 ∩ cin 3539 ⊆ wss 3540 {csn 4125 {cpr 4127 class class class wbr 4583 dom cdm 5038 ↾ cres 5040 “ cima 5041 Fun wfun 5798 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 0cc0 9815 1c1 9816 + caddc 9818 ℤ_≥cuz 11563 ...cfz 12197 ..^cfzo 12334 #chash 12979 Word cword 13146 Vtxcvtx 25673 iEdgciedg 25674 1Walksc1wlks 40796

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-ifp 1007 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-card 8648 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-n0 11170 df-z 11255 df-uz 11564 df-fz 12198 df-fzo 12335 df-hash 12980 df-word 13154 df-substr 13158 df-1wlks 40800

This theorem is referenced by: trlres 40908 eupthres 41383

W3C validator