wkslem1 - Metamath Proof Explorer

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

Theorem wkslem1 30200

Description: Lemma 1 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021.)

**Assertion**
Ref	Expression
wkslem1	⊢ (𝐴 = 𝐵 → (if-((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)), (𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)}, {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴))) ↔ if-((𝑃‘𝐵) = (𝑃‘(𝐵 + 1)), (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}, {(𝑃‘𝐵), (𝑃‘(𝐵 + 1))} ⊆ (𝐼‘(𝐹‘𝐵)))))

**Proof of Theorem wkslem1**
Step	Hyp	Ref	Expression
1		fveq2 6893	. . 3 ⊢ (𝐴 = 𝐵 → (𝑃‘𝐴) = (𝑃‘𝐵))
2		fvoveq1 7450	. . 3 ⊢ (𝐴 = 𝐵 → (𝑃‘(𝐴 + 1)) = (𝑃‘(𝐵 + 1)))
3	1, 2	eqeq12d 2779	. 2 ⊢ (𝐴 = 𝐵 → ((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)) ↔ (𝑃‘𝐵) = (𝑃‘(𝐵 + 1))))
4		2fveq3 6898	. . 3 ⊢ (𝐴 = 𝐵 → (𝐼‘(𝐹‘𝐴)) = (𝐼‘(𝐹‘𝐵)))
5	1	sneqd 4595	. . 3 ⊢ (𝐴 = 𝐵 → {(𝑃‘𝐴)} = {(𝑃‘𝐵)})
6	4, 5	eqeq12d 2779	. 2 ⊢ (𝐴 = 𝐵 → ((𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)} ↔ (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}))
7	1, 2	preq12d 4701	. . 3 ⊢ (𝐴 = 𝐵 → {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} = {(𝑃‘𝐵), (𝑃‘(𝐵 + 1))})
8	7, 4	sseq12d 3945	. 2 ⊢ (𝐴 = 𝐵 → ({(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴)) ↔ {(𝑃‘𝐵), (𝑃‘(𝐵 + 1))} ⊆ (𝐼‘(𝐹‘𝐵))))
9	3, 6, 8	ifpbi123d 1095	1 ⊢ (𝐴 = 𝐵 → (if-((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)), (𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)}, {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴))) ↔ if-((𝑃‘𝐵) = (𝑃‘(𝐵 + 1)), (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}, {(𝑃‘𝐵), (𝑃‘(𝐵 + 1))} ⊆ (𝐼‘(𝐹‘𝐵)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 if-wif 1078 = wceq 1569 ⊆ wss 3899 {csn 4587 {cpr 4589 ‘cfv 6546 (class class class)co 7427 1c1 11211 + caddc 11213

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-ext 2735

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-ifp 1079 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-sb 2101 df-clab 2742 df-cleq 2755 df-clel 2838 df-rab 3416 df-v 3455 df-ss 3900 df-dif 4049 df-un 4153 df-nul 4281 df-if 4485 df-sn 4588 df-pr 4590 df-op 4838 df-uni 4870 df-br 5106 df-iota 6500 df-fv 6554 df-ov 7430

This theorem is used by: wlk1walk 30231 wlkres 30261 wlkp1lem8 30271 pfxwlk 30278 revwlk 30279 crctcshwlkn0lem6 30416 crctcshwlkn0lem7 30417 crctcshwlkn0 30422

W3C validator