Metamath Proof Explorer


Theorem 2wlkdlem8

Description: Lemma 8 for 2wlkd . (Contributed by AV, 14-Feb-2021)

Ref Expression
Hypotheses 2wlkd.p P = ⟨“ ABC ”⟩
2wlkd.f F = ⟨“ JK ”⟩
2wlkd.s φ A V B V C V
2wlkd.n φ A B B C
2wlkd.e φ A B I J B C I K
Assertion 2wlkdlem8 φ F 0 = J F 1 = K

Proof

Step Hyp Ref Expression
1 2wlkd.p P = ⟨“ ABC ”⟩
2 2wlkd.f F = ⟨“ JK ”⟩
3 2wlkd.s φ A V B V C V
4 2wlkd.n φ A B B C
5 2wlkd.e φ A B I J B C I K
6 1 2 3 4 5 2wlkdlem7 φ J V K V
7 s2fv0 J V ⟨“ JK ”⟩ 0 = J
8 s2fv1 K V ⟨“ JK ”⟩ 1 = K
9 7 8 anim12i J V K V ⟨“ JK ”⟩ 0 = J ⟨“ JK ”⟩ 1 = K
10 6 9 syl φ ⟨“ JK ”⟩ 0 = J ⟨“ JK ”⟩ 1 = K
11 2 fveq1i F 0 = ⟨“ JK ”⟩ 0
12 11 eqeq1i F 0 = J ⟨“ JK ”⟩ 0 = J
13 2 fveq1i F 1 = ⟨“ JK ”⟩ 1
14 13 eqeq1i F 1 = K ⟨“ JK ”⟩ 1 = K
15 12 14 anbi12i F 0 = J F 1 = K ⟨“ JK ”⟩ 0 = J ⟨“ JK ”⟩ 1 = K
16 10 15 sylibr φ F 0 = J F 1 = K