Theorem wlkresOLD 27021

Description: Obsolete version of wlkres 27019 as of 30-Nov-2022. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
wlkresOLD	⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄)

Proof of Theorem wlkresOLD

Dummy variables 𝑘 𝑖 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wlkresOLD.h	. . 3 ⊢ 𝐻 = (𝐹 ↾ (0..^𝑁))
2		wlkresOLD.d	. . . . . . . 8 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
3		wlkresOLD.i	. . . . . . . . 9 ⊢ 𝐼 = (iEdg‘𝐺)
4	3	wlkf 26962	. . . . . . . 8 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
5		wrdfn 13614	. . . . . . . 8 ⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹 Fn (0..^(♯‘𝐹)))
6	2, 4, 5	3syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐹 Fn (0..^(♯‘𝐹)))
7		wlkresOLD.n	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))
8		elfzouz2 12803	. . . . . . . 8 ⊢ (𝑁 ∈ (0..^(♯‘𝐹)) → (♯‘𝐹) ∈ (ℤ≥‘𝑁))
9		fzoss2 12815	. . . . . . . 8 ⊢ ((♯‘𝐹) ∈ (ℤ≥‘𝑁) → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
10	7, 8, 9	3syl 18	. . . . . . 7 ⊢ (𝜑 → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
11		fnssres 6250	. . . . . . 7 ⊢ ((𝐹 Fn (0..^(♯‘𝐹)) ∧ (0..^𝑁) ⊆ (0..^(♯‘𝐹))) → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
12	6, 10, 11	syl2anc 579	. . . . . 6 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁))
13		simpr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
14		fveqeq2 6455	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑥 → ((𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
15	14	adantl 475	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) ∧ 𝑖 = 𝑥) → ((𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥) ↔ (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
16		fvres 6465	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (0..^𝑁) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹‘𝑥))
17	16	adantl 475	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) = (𝐹‘𝑥))
18	17	eqcomd 2783	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
19	13, 15, 18	rspcedvd 3517	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ∃𝑖 ∈ (0..^𝑁)(𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
20	6	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝐹 Fn (0..^(♯‘𝐹)))
21	10	adantr 474	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ (0..^(♯‘𝐹)))
22	20, 21	fvelimabd 6514	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)) ↔ ∃𝑖 ∈ (0..^𝑁)(𝐹‘𝑖) = ((𝐹 ↾ (0..^𝑁))‘𝑥)))
23	19, 22	mpbird 249	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ (𝐹 “ (0..^𝑁)))
24	2, 4	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼)
25		wrdf 13604	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Word dom 𝐼 → 𝐹:(0..^(♯‘𝐹))⟶dom 𝐼)
26		ffvelrn 6621	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 ∧ 𝑥 ∈ (0..^(♯‘𝐹))) → (𝐹‘𝑥) ∈ dom 𝐼)
27	26	expcom 404	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (0..^(♯‘𝐹)) → (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → (𝐹‘𝑥) ∈ dom 𝐼))
28	10	sselda 3820	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^(♯‘𝐹)))
29	27, 28	syl11 33	. . . . . . . . . . . . . . 15 ⊢ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) ∈ dom 𝐼))
30	29	expd 406	. . . . . . . . . . . . . 14 ⊢ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ dom 𝐼)))
31	25, 30	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ dom 𝐼)))
32	24, 31	mpcom 38	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐹‘𝑥) ∈ dom 𝐼))
33	32	imp 397	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐹‘𝑥) ∈ dom 𝐼)
34	17, 33	eqeltrd 2858	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom 𝐼)
35	23, 34	elind 4020	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼))
36		dmres 5668	. . . . . . . . 9 ⊢ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))) = ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼)
37	35, 36	syl6eleqr 2869	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
38		wlkresOLD.e	. . . . . . . . . . 11 ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
39	38	dmeqd 5571	. . . . . . . . . 10 ⊢ (𝜑 → dom (iEdg‘𝑆) = dom (𝐼 ↾ (𝐹 “ (0..^𝑁))))
40	39	eleq2d 2844	. . . . . . . . 9 ⊢ (𝜑 → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
41	40	adantr 474	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (𝐼 ↾ (𝐹 “ (0..^𝑁)))))
42	37, 41	mpbird 249	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
43	42	ralrimiva 3147	. . . . . 6 ⊢ (𝜑 → ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆))
44		ffnfv 6652	. . . . . 6 ⊢ ((𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆) ↔ ((𝐹 ↾ (0..^𝑁)) Fn (0..^𝑁) ∧ ∀𝑥 ∈ (0..^𝑁)((𝐹 ↾ (0..^𝑁))‘𝑥) ∈ dom (iEdg‘𝑆)))
45	12, 43, 44	sylanbrc 578	. . . . 5 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆))
46		fzossfz 12807	. . . . . . . . 9 ⊢ (0..^(♯‘𝐹)) ⊆ (0...(♯‘𝐹))
47	46, 7	sseldi 3818	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ (0...(♯‘𝐹)))
48		wlkreslem0OLD 27016	. . . . . . . 8 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑁 ∈ (0...(♯‘𝐹))) → (♯‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
49	24, 47, 48	syl2anc 579	. . . . . . 7 ⊢ (𝜑 → (♯‘(𝐹 ↾ (0..^𝑁))) = 𝑁)
50	49	oveq2d 6938	. . . . . 6 ⊢ (𝜑 → (0..^(♯‘(𝐹 ↾ (0..^𝑁)))) = (0..^𝑁))
51	50	feq2d 6277	. . . . 5 ⊢ (𝜑 → ((𝐹 ↾ (0..^𝑁)):(0..^(♯‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^𝑁)⟶dom (iEdg‘𝑆)))
52	45, 51	mpbird 249	. . . 4 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)):(0..^(♯‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
53		iswrdb 13605	. . . 4 ⊢ ((𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆) ↔ (𝐹 ↾ (0..^𝑁)):(0..^(♯‘(𝐹 ↾ (0..^𝑁))))⟶dom (iEdg‘𝑆))
54	52, 53	sylibr 226	. . 3 ⊢ (𝜑 → (𝐹 ↾ (0..^𝑁)) ∈ Word dom (iEdg‘𝑆))
55	1, 54	syl5eqel 2862	. 2 ⊢ (𝜑 → 𝐻 ∈ Word dom (iEdg‘𝑆))
56		wlkresOLD.v	. . . . . . . 8 ⊢ 𝑉 = (Vtx‘𝐺)
57	56	wlkp 26964	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
58	2, 57	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉)
59		wlkresOLD.s	. . . . . . 7 ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)
60	59	feq3d 6278	. . . . . 6 ⊢ (𝜑 → (𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆) ↔ 𝑃:(0...(♯‘𝐹))⟶𝑉))
61	58, 60	mpbird 249	. . . . 5 ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝑆))
62		elfzuz3 12656	. . . . . 6 ⊢ (𝑁 ∈ (0...(♯‘𝐹)) → (♯‘𝐹) ∈ (ℤ≥‘𝑁))
63		fzss2 12698	. . . . . 6 ⊢ ((♯‘𝐹) ∈ (ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...(♯‘𝐹)))
64	47, 62, 63	3syl 18	. . . . 5 ⊢ (𝜑 → (0...𝑁) ⊆ (0...(♯‘𝐹)))
65	61, 64	fssresd 6321	. . . 4 ⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆))
66	1	fveq2i 6449	. . . . . . 7 ⊢ (♯‘𝐻) = (♯‘(𝐹 ↾ (0..^𝑁)))
67	66, 49	syl5eq 2825	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) = 𝑁)
68	67	oveq2d 6938	. . . . 5 ⊢ (𝜑 → (0...(♯‘𝐻)) = (0...𝑁))
69	68	feq2d 6277	. . . 4 ⊢ (𝜑 → ((𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶(Vtx‘𝑆)))
70	65, 69	mpbird 249	. . 3 ⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆))
71		wlkresOLD.q	. . . 4 ⊢ 𝑄 = (𝑃 ↾ (0...𝑁))
72	71	feq1i 6282	. . 3 ⊢ (𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ↔ (𝑃 ↾ (0...𝑁)):(0...(♯‘𝐻))⟶(Vtx‘𝑆))
73	70, 72	sylibr 226	. 2 ⊢ (𝜑 → 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆))
74		wlkv 26960	. . . . . . 7 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V))
75	56, 3	iswlk 26958	. . . . . . . 8 ⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
76	75	biimpd 221	. . . . . . 7 ⊢ ((𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
77	74, 76	mpcom 38	. . . . . 6 ⊢ (𝐹(Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
78	2, 77	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
79	78	adantr 474	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
80	67	oveq2d 6938	. . . . . . . . . . 11 ⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^𝑁))
81	80	eleq2d 2844	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) ↔ 𝑥 ∈ (0..^𝑁)))
82	71	fveq1i 6447	. . . . . . . . . . . . 13 ⊢ (𝑄‘𝑥) = ((𝑃 ↾ (0...𝑁))‘𝑥)
83		fzossfz 12807	. . . . . . . . . . . . . . . 16 ⊢ (0..^𝑁) ⊆ (0...𝑁)
84	83	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (0..^𝑁) ⊆ (0...𝑁))
85	84	sselda 3820	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0...𝑁))
86	85	fvresd 6466	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘𝑥) = (𝑃‘𝑥))
87	82, 86	syl5req 2826	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘𝑥) = (𝑄‘𝑥))
88	71	fveq1i 6447	. . . . . . . . . . . . 13 ⊢ (𝑄‘(𝑥 + 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1))
89		fzofzp1 12884	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (0..^𝑁) → (𝑥 + 1) ∈ (0...𝑁))
90	89	adantl 475	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑥 + 1) ∈ (0...𝑁))
91	90	fvresd 6466	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃 ↾ (0...𝑁))‘(𝑥 + 1)) = (𝑃‘(𝑥 + 1)))
92	88, 91	syl5req 2826	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))
93	87, 92	jca 507	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
94	93	ex 403	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
95	81, 94	sylbid 232	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1)))))
96	95	imp 397	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → ((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))))
97	24	ancli 544	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝜑 ∧ 𝐹 ∈ Word dom 𝐼))
98	25	ffund 6295	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Word dom 𝐼 → Fun 𝐹)
99	98	adantl 475	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → Fun 𝐹)
100	99	adantr 474	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → Fun 𝐹)
101		fdm 6299	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹:(0..^(♯‘𝐹))⟶dom 𝐼 → dom 𝐹 = (0..^(♯‘𝐹)))
102		sseq2 3845	. . . . . . . . . . . . . . . . . . 19 ⊢ (dom 𝐹 = (0..^(♯‘𝐹)) → ((0..^𝑁) ⊆ dom 𝐹 ↔ (0..^𝑁) ⊆ (0..^(♯‘𝐹))))
103	10, 102	syl5ibr 238	. . . . . . . . . . . . . . . . . 18 ⊢ (dom 𝐹 = (0..^(♯‘𝐹)) → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
104	25, 101, 103	3syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐹 ∈ Word dom 𝐼 → (𝜑 → (0..^𝑁) ⊆ dom 𝐹))
105	104	impcom 398	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) → (0..^𝑁) ⊆ dom 𝐹)
106	105	adantr 474	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → (0..^𝑁) ⊆ dom 𝐹)
107		simpr 479	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → 𝑥 ∈ (0..^𝑁))
108	100, 106, 107	resfvresima 6767	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝐹 ∈ Word dom 𝐼) ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
109	97, 108	sylan 575	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
110	109	eqcomd 2783	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^𝑁)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
111	110	ex 403	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑥 ∈ (0..^𝑁) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
112	81, 111	sylbid 232	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 ∈ (0..^(♯‘𝐻)) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥))))
113	112	imp 397	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
114	38	adantr 474	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))
115	1	fveq1i 6447	. . . . . . . . . . 11 ⊢ (𝐻‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥)
116	115	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐻‘𝑥) = ((𝐹 ↾ (0..^𝑁))‘𝑥))
117	114, 116	fveq12d 6453	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → ((iEdg‘𝑆)‘(𝐻‘𝑥)) = ((𝐼 ↾ (𝐹 “ (0..^𝑁)))‘((𝐹 ↾ (0..^𝑁))‘𝑥)))
118	113, 117	eqtr4d 2816	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥)))
119	96, 118	jca 507	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))))
120	7, 8	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝐹) ∈ (ℤ≥‘𝑁))
121	1	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻 = (𝐹 ↾ (0..^𝑁)))
122	121	fveq2d 6450	. . . . . . . . . . . . 13 ⊢ (𝜑 → (♯‘𝐻) = (♯‘(𝐹 ↾ (0..^𝑁))))
123	122, 49	eqtrd 2813	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝐻) = 𝑁)
124	123	fveq2d 6450	. . . . . . . . . . 11 ⊢ (𝜑 → (ℤ≥‘(♯‘𝐻)) = (ℤ≥‘𝑁))
125	120, 124	eleqtrrd 2861	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝐹) ∈ (ℤ≥‘(♯‘𝐻)))
126		fzoss2 12815	. . . . . . . . . 10 ⊢ ((♯‘𝐹) ∈ (ℤ≥‘(♯‘𝐻)) → (0..^(♯‘𝐻)) ⊆ (0..^(♯‘𝐹)))
127	125, 126	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (0..^(♯‘𝐻)) ⊆ (0..^(♯‘𝐹)))
128	127	sselda 3820	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → 𝑥 ∈ (0..^(♯‘𝐹)))
129		wkslem1 26955	. . . . . . . . 9 ⊢ (𝑘 = 𝑥 → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)))))
130	129	rspcv 3506	. . . . . . . 8 ⊢ (𝑥 ∈ (0..^(♯‘𝐹)) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)))))
131	128, 130	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)))))
132		eqeq12 2790	. . . . . . . . . 10 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1))))
133	132	adantr 474	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)) ↔ (𝑄‘𝑥) = (𝑄‘(𝑥 + 1))))
134		simpr 479	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥)))
135		sneq 4407	. . . . . . . . . . . 12 ⊢ ((𝑃‘𝑥) = (𝑄‘𝑥) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
136	135	adantr 474	. . . . . . . . . . 11 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
137	136	adantr 474	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥)} = {(𝑄‘𝑥)})
138	134, 137	eqeq12d 2792	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ((𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)} ↔ ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}))
139		preq12 4501	. . . . . . . . . . 11 ⊢ (((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))})
140	139	adantr 474	. . . . . . . . . 10 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} = {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))})
141	140, 134	sseq12d 3852	. . . . . . . . 9 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → ({(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥)) ↔ {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
142	133, 138, 141	ifpbi123d 1061	. . . . . . . 8 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))) ↔ if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
143	142	biimpd 221	. . . . . . 7 ⊢ ((((𝑃‘𝑥) = (𝑄‘𝑥) ∧ (𝑃‘(𝑥 + 1)) = (𝑄‘(𝑥 + 1))) ∧ (𝐼‘(𝐹‘𝑥)) = ((iEdg‘𝑆)‘(𝐻‘𝑥))) → (if-((𝑃‘𝑥) = (𝑃‘(𝑥 + 1)), (𝐼‘(𝐹‘𝑥)) = {(𝑃‘𝑥)}, {(𝑃‘𝑥), (𝑃‘(𝑥 + 1))} ⊆ (𝐼‘(𝐹‘𝑥))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
144	119, 131, 143	sylsyld 61	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
145	144	com12 32	. . . . 5 ⊢ (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
146	145	3ad2ant3 1126	. . . 4 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) → ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥)))))
147	79, 146	mpcom 38	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (0..^(♯‘𝐻))) → if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
148	147	ralrimiva 3147	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))
149	56, 3, 2, 7, 59, 38, 1, 71	wlkreslemOLD 27020	. . 3 ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V))
150		eqid 2777	. . . 4 ⊢ (Vtx‘𝑆) = (Vtx‘𝑆)
151		eqid 2777	. . . 4 ⊢ (iEdg‘𝑆) = (iEdg‘𝑆)
152	150, 151	iswlk 26958	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V) → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))))
153	149, 152	syl 17	. 2 ⊢ (𝜑 → (𝐻(Walks‘𝑆)𝑄 ↔ (𝐻 ∈ Word dom (iEdg‘𝑆) ∧ 𝑄:(0...(♯‘𝐻))⟶(Vtx‘𝑆) ∧ ∀𝑥 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑥) = (𝑄‘(𝑥 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑥)) = {(𝑄‘𝑥)}, {(𝑄‘𝑥), (𝑄‘(𝑥 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑥))))))
154	55, 73, 148, 153	mpbir3and 1399	1 ⊢ (𝜑 → 𝐻(Walks‘𝑆)𝑄)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386  if-wif 1046   ∧ w3a 1071   = wceq 1601   ∈ wcel 2106  ∀wral 3089  ∃wrex 3090  Vcvv 3397   ∩ cin 3790   ⊆ wss 3791  {csn 4397  {cpr 4399   class class class wbr 4886  dom cdm 5355   ↾ cres 5357   “ cima 5358  Fun wfun 6129   Fn wfn 6130  ⟶wf 6131  ‘cfv 6135  (class class class)co 6922  0cc0 10272  1c1 10273   + caddc 10275  ℤ_≥cuz 11992  ...cfz 12643  ..^cfzo 12784  ♯chash 13435  Word cword 13599  Vtxcvtx 26344  iEdgciedg 26345  Walkscwlks 26944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ifp 1047  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-nel 3075  df-ral 3094  df-rex 3095  df-reu 3096  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-card 9098  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-nn 11375  df-n0 11643  df-z 11729  df-uz 11993  df-fz 12644  df-fzo 12785  df-hash 13436  df-word 13600  df-substr 13731  df-pfx 13780  df-wlks 26947

This theorem is referenced by:  trlresOLD  27053  eupthresOLD  27632