wlkp1lem8 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > wlkp1lem8		Structured version Visualization version GIF version

Theorem wlkp1lem8 29660

Description: Lemma for wlkp1 29661. (Contributed by AV, 6-Mar-2021.)

**Hypotheses**
Ref	Expression
wlkp1.v	⊢ 𝑉 = (Vtx‘𝐺)
wlkp1.i	⊢ 𝐼 = (iEdg‘𝐺)
wlkp1.f	⊢ (𝜑 → Fun 𝐼)
wlkp1.a	⊢ (𝜑 → 𝐼 ∈ Fin)
wlkp1.b	⊢ (𝜑 → 𝐵 ∈ 𝑊)
wlkp1.c	⊢ (𝜑 → 𝐶 ∈ 𝑉)
wlkp1.d	⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)
wlkp1.w	⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
wlkp1.n	⊢ 𝑁 = (♯‘𝐹)
wlkp1.e	⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))
wlkp1.x	⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)
wlkp1.u	⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))
wlkp1.h	⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})
wlkp1.q	⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})
wlkp1.s	⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)
wlkp1.l	⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶})

**Assertion**
Ref	Expression
wlkp1lem8	⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))

Distinct variable groups: 𝜑,𝑘 𝑘,𝑁 𝑃,𝑘 𝑄,𝑘 𝑘,𝐹 𝑘,𝐺 𝑘,𝐻 𝑆,𝑘 Allowed substitution hints: 𝐵(𝑘) 𝐶(𝑘) 𝐸(𝑘) 𝐼(𝑘) 𝑉(𝑘) 𝑊(𝑘)

Proof of Theorem wlkp1lem8 Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		wlkp1.v	. . . 4 ⊢ 𝑉 = (Vtx‘𝐺)
2		wlkp1.i	. . . 4 ⊢ 𝐼 = (iEdg‘𝐺)
3		wlkp1.f	. . . 4 ⊢ (𝜑 → Fun 𝐼)
4		wlkp1.a	. . . 4 ⊢ (𝜑 → 𝐼 ∈ Fin)
5		wlkp1.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
6		wlkp1.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
7		wlkp1.d	. . . 4 ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)
8		wlkp1.w	. . . 4 ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
9		wlkp1.n	. . . 4 ⊢ 𝑁 = (♯‘𝐹)
10		wlkp1.e	. . . 4 ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))
11		wlkp1.x	. . . 4 ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)
12		wlkp1.u	. . . 4 ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩}))
13		wlkp1.h	. . . 4 ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})
14		wlkp1.q	. . . 4 ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})
15		wlkp1.s	. . . 4 ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉)
16	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15	wlkp1lem6 29658	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))))
17	10	elfvexd 6915	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ V)
18	1, 2	iswlkg 29593	. . . . . 6 ⊢ (𝐺 ∈ V → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
19	17, 18	syl 17	. . . . 5 ⊢ (𝜑 → (𝐹(Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))))
20	9	eqcomi 2744	. . . . . . . . 9 ⊢ (♯‘𝐹) = 𝑁
21	20	oveq2i 7416	. . . . . . . 8 ⊢ (0..^(♯‘𝐹)) = (0..^𝑁)
22	21	raleqi 3303	. . . . . . 7 ⊢ (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ↔ ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
23	22	biimpi 216	. . . . . 6 ⊢ (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
24	23	3ad2ant3 1135	. . . . 5 ⊢ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
25	19, 24	biimtrdi 253	. . . 4 ⊢ (𝜑 → (𝐹(Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
26	8, 25	mpd 15	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
27		eqeq12 2752	. . . . . . 7 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))) → ((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)) ↔ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1))))
28	27	3adant3 1132	. . . . . 6 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → ((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)) ↔ (𝑃‘𝑘) = (𝑃‘(𝑘 + 1))))
29		simp3 1138	. . . . . . 7 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘)))
30		simp1 1136	. . . . . . . 8 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → (𝑄‘𝑘) = (𝑃‘𝑘))
31	30	sneqd 4613	. . . . . . 7 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → {(𝑄‘𝑘)} = {(𝑃‘𝑘)})
32	29, 31	eqeq12d 2751	. . . . . 6 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → (((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)} ↔ (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}))
33		preq12 4711	. . . . . . . 8 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1))) → {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})
34	33	3adant3 1132	. . . . . . 7 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})
35	34, 29	sseq12d 3992	. . . . . 6 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → ({(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)) ↔ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))
36	28, 32, 35	ifpbi123d 1078	. . . . 5 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → (if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))
37	36	biimprd 248	. . . 4 ⊢ (((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → (if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))))
38	37	ral2imi 3075	. . 3 ⊢ (∀𝑘 ∈ (0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘))) → (∀𝑘 ∈ (0..^𝑁)if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) → ∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))))
39	16, 26, 38	sylc 65	. 2 ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))
40	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	wlkp1lem3 29655	. . . . 5 ⊢ (𝜑 → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘𝐵))
41	40	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘𝐵))
42	5, 10, 7	3jca 1128	. . . . . 6 ⊢ (𝜑 → (𝐵 ∈ 𝑊 ∧ 𝐸 ∈ (Edg‘𝐺) ∧ ¬ 𝐵 ∈ dom 𝐼))
43	42	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → (𝐵 ∈ 𝑊 ∧ 𝐸 ∈ (Edg‘𝐺) ∧ ¬ 𝐵 ∈ dom 𝐼))
44		fsnunfv 7179	. . . . 5 ⊢ ((𝐵 ∈ 𝑊 ∧ 𝐸 ∈ (Edg‘𝐺) ∧ ¬ 𝐵 ∈ dom 𝐼) → ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘𝐵) = 𝐸)
45	43, 44	syl 17	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → ((𝐼 ∪ {⟨𝐵, 𝐸⟩})‘𝐵) = 𝐸)
46		fveq2 6876	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝑄‘𝑥) = (𝑄‘𝑁))
47		fveq2 6876	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝑃‘𝑥) = (𝑃‘𝑁))
48	46, 47	eqeq12d 2751	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝑄‘𝑥) = (𝑃‘𝑥) ↔ (𝑄‘𝑁) = (𝑃‘𝑁)))
49	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15	wlkp1lem5 29657	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (0...𝑁)(𝑄‘𝑥) = (𝑃‘𝑥))
50	2	wlkf 29594	. . . . . . . . . 10 ⊢ (𝐹(Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼)
51		lencl 14551	. . . . . . . . . . 11 ⊢ (𝐹 ∈ Word dom 𝐼 → (♯‘𝐹) ∈ ℕ₀)
52	9	eleq1i 2825	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ ↔ (♯‘𝐹) ∈ ℕ₀)
53		elnn0uz 12897	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ ↔ 𝑁 ∈ (ℤ_≥‘0))
54	52, 53	sylbb1 237	. . . . . . . . . . 11 ⊢ ((♯‘𝐹) ∈ ℕ₀ → 𝑁 ∈ (ℤ_≥‘0))
55	51, 54	syl 17	. . . . . . . . . 10 ⊢ (𝐹 ∈ Word dom 𝐼 → 𝑁 ∈ (ℤ_≥‘0))
56	8, 50, 55	3syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘0))
57	56, 53	sylibr 234	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
58		nn0fz0 13642	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ ↔ 𝑁 ∈ (0...𝑁))
59	57, 58	sylib 218	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ (0...𝑁))
60	48, 49, 59	rspcdva 3602	. . . . . 6 ⊢ (𝜑 → (𝑄‘𝑁) = (𝑃‘𝑁))
61	14	fveq1i 6877	. . . . . . . . . . 11 ⊢ (𝑄‘(𝑁 + 1)) = ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑁 + 1))
62		ovex 7438	. . . . . . . . . . . 12 ⊢ (𝑁 + 1) ∈ V
63	1, 2, 3, 4, 5, 6, 7, 8, 9	wlkp1lem1 29653	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ (𝑁 + 1) ∈ dom 𝑃)
64		fsnunfv 7179	. . . . . . . . . . . 12 ⊢ (((𝑁 + 1) ∈ V ∧ 𝐶 ∈ 𝑉 ∧ ¬ (𝑁 + 1) ∈ dom 𝑃) → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑁 + 1)) = 𝐶)
65	62, 6, 63, 64	mp3an2i 1468	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})‘(𝑁 + 1)) = 𝐶)
66	61, 65	eqtrid 2782	. . . . . . . . . 10 ⊢ (𝜑 → (𝑄‘(𝑁 + 1)) = 𝐶)
67	66	eqeq2d 2746	. . . . . . . . 9 ⊢ (𝜑 → ((𝑃‘𝑁) = (𝑄‘(𝑁 + 1)) ↔ (𝑃‘𝑁) = 𝐶))
68		eqcom 2742	. . . . . . . . 9 ⊢ ((𝑃‘𝑁) = 𝐶 ↔ 𝐶 = (𝑃‘𝑁))
69	67, 68	bitrdi 287	. . . . . . . 8 ⊢ (𝜑 → ((𝑃‘𝑁) = (𝑄‘(𝑁 + 1)) ↔ 𝐶 = (𝑃‘𝑁)))
70		wlkp1.l	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶})
71		sneq 4611	. . . . . . . . . . 11 ⊢ (𝐶 = (𝑃‘𝑁) → {𝐶} = {(𝑃‘𝑁)})
72	71	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → {𝐶} = {(𝑃‘𝑁)})
73	70, 72	eqtrd 2770	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {(𝑃‘𝑁)})
74	73	ex 412	. . . . . . . 8 ⊢ (𝜑 → (𝐶 = (𝑃‘𝑁) → 𝐸 = {(𝑃‘𝑁)}))
75	69, 74	sylbid 240	. . . . . . 7 ⊢ (𝜑 → ((𝑃‘𝑁) = (𝑄‘(𝑁 + 1)) → 𝐸 = {(𝑃‘𝑁)}))
76		eqeq1 2739	. . . . . . . 8 ⊢ ((𝑄‘𝑁) = (𝑃‘𝑁) → ((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)) ↔ (𝑃‘𝑁) = (𝑄‘(𝑁 + 1))))
77		sneq 4611	. . . . . . . . 9 ⊢ ((𝑄‘𝑁) = (𝑃‘𝑁) → {(𝑄‘𝑁)} = {(𝑃‘𝑁)})
78	77	eqeq2d 2746	. . . . . . . 8 ⊢ ((𝑄‘𝑁) = (𝑃‘𝑁) → (𝐸 = {(𝑄‘𝑁)} ↔ 𝐸 = {(𝑃‘𝑁)}))
79	76, 78	imbi12d 344	. . . . . . 7 ⊢ ((𝑄‘𝑁) = (𝑃‘𝑁) → (((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)) → 𝐸 = {(𝑄‘𝑁)}) ↔ ((𝑃‘𝑁) = (𝑄‘(𝑁 + 1)) → 𝐸 = {(𝑃‘𝑁)})))
80	75, 79	syl5ibrcom 247	. . . . . 6 ⊢ (𝜑 → ((𝑄‘𝑁) = (𝑃‘𝑁) → ((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)) → 𝐸 = {(𝑄‘𝑁)})))
81	60, 80	mpd 15	. . . . 5 ⊢ (𝜑 → ((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)) → 𝐸 = {(𝑄‘𝑁)}))
82	81	imp 406	. . . 4 ⊢ ((𝜑 ∧ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → 𝐸 = {(𝑄‘𝑁)})
83	41, 45, 82	3eqtrd 2774	. . 3 ⊢ ((𝜑 ∧ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)})
84	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15	wlkp1lem7 29659	. . . 4 ⊢ (𝜑 → {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))
85	84	adantr 480	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑄‘𝑁) = (𝑄‘(𝑁 + 1))) → {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))
86	83, 85	ifpimpda 1080	. 2 ⊢ (𝜑 → if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁))))
87	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	wlkp1lem2 29654	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) = (𝑁 + 1))
88	87	oveq2d 7421	. . . . 5 ⊢ (𝜑 → (0..^(♯‘𝐻)) = (0..^(𝑁 + 1)))
89		fzosplitsn 13791	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
90	56, 89	syl 17	. . . . 5 ⊢ (𝜑 → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁}))
91	88, 90	eqtrd 2770	. . . 4 ⊢ (𝜑 → (0..^(♯‘𝐻)) = ((0..^𝑁) ∪ {𝑁}))
92	91	raleqdv 3305	. . 3 ⊢ (𝜑 → (∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ ∀𝑘 ∈ ((0..^𝑁) ∪ {𝑁})if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))))
93		ralunb 4172	. . . 4 ⊢ (∀𝑘 ∈ ((0..^𝑁) ∪ {𝑁})if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ (∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ∧ ∀𝑘 ∈ {𝑁}if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))))
94	93	a1i 11	. . 3 ⊢ (𝜑 → (∀𝑘 ∈ ((0..^𝑁) ∪ {𝑁})if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ (∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ∧ ∀𝑘 ∈ {𝑁}if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))))
95	9	fvexi 6890	. . . . 5 ⊢ 𝑁 ∈ V
96		wkslem1 29587	. . . . . 6 ⊢ (𝑘 = 𝑁 → (if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))))
97	96	ralsng 4651	. . . . 5 ⊢ (𝑁 ∈ V → (∀𝑘 ∈ {𝑁}if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))))
98	95, 97	mp1i 13	. . . 4 ⊢ (𝜑 → (∀𝑘 ∈ {𝑁}if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁)))))
99	98	anbi2d 630	. . 3 ⊢ (𝜑 → ((∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ∧ ∀𝑘 ∈ {𝑁}if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))) ↔ (∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ∧ if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁))))))
100	92, 94, 99	3bitrd 305	. 2 ⊢ (𝜑 → (∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ↔ (∀𝑘 ∈ (0..^𝑁)if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))) ∧ if-((𝑄‘𝑁) = (𝑄‘(𝑁 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑁)) = {(𝑄‘𝑁)}, {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁))))))
101	39, 86, 100	mpbir2and 713	1 ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 if-wif 1062 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ∀wral 3051 Vcvv 3459 ∪ cun 3924 ⊆ wss 3926 {csn 4601 {cpr 4603 ⟨cop 4607 class class class wbr 5119 dom cdm 5654 Fun wfun 6525 ⟶wf 6527 ‘cfv 6531 (class class class)co 7405 Fincfn 8959 0cc0 11129 1c1 11130 + caddc 11132 ℕ₀cn0 12501 ℤ_≥cuz 12852 ...cfz 13524 ..^cfzo 13671 ♯chash 14348 Word cword 14531 Vtxcvtx 28975 iEdgciedg 28976 Edgcedg 29026 Walkscwlks 29576

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ifp 1063 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-oadd 8484 df-er 8719 df-map 8842 df-pm 8843 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-dju 9915 df-card 9953 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-nn 12241 df-n0 12502 df-z 12589 df-uz 12853 df-fz 13525 df-fzo 13672 df-hash 14349 df-word 14532 df-wlks 29579

This theorem is referenced by: wlkp1 29661

W3C validator