Metamath Proof Explorer

Theorem 3wlkdlem9

Description: Lemma 9 for 3wlkd . (Contributed by AV, 7-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p ⊢P=⟨“ABCD”⟩
3wlkd.f ⊢F=⟨“JKL”⟩
3wlkd.s ⊢φ→A∈V∧B∈V∧C∈V∧D∈V
3wlkd.n ⊢φ→A≠B∧A≠C∧B≠C∧B≠D∧C≠D
3wlkd.e ⊢φ→AB⊆I⁡J∧BC⊆I⁡K∧CD⊆I⁡L
Assertion 3wlkdlem9 ⊢φ→AB⊆I⁡F⁡0∧BC⊆I⁡F⁡1∧CD⊆I⁡F⁡2

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢P=⟨“ABCD”⟩
2 3wlkd.f ⊢F=⟨“JKL”⟩
3 3wlkd.s ⊢φ→A∈V∧B∈V∧C∈V∧D∈V
4 3wlkd.n ⊢φ→A≠B∧A≠C∧B≠C∧B≠D∧C≠D
5 3wlkd.e ⊢φ→AB⊆I⁡J∧BC⊆I⁡K∧CD⊆I⁡L
6 1 2 3 4 5 3wlkdlem8 ⊢φ→F⁡0=J∧F⁡1=K∧F⁡2=L
7 fveq2 ⊢F⁡0=J→I⁡F⁡0=I⁡J
8 7 sseq2d ⊢F⁡0=J→AB⊆I⁡F⁡0↔AB⊆I⁡J
9 8 3ad2ant1 ⊢F⁡0=J∧F⁡1=K∧F⁡2=L→AB⊆I⁡F⁡0↔AB⊆I⁡J
10 fveq2 ⊢F⁡1=K→I⁡F⁡1=I⁡K
11 10 sseq2d ⊢F⁡1=K→BC⊆I⁡F⁡1↔BC⊆I⁡K
12 11 3ad2ant2 ⊢F⁡0=J∧F⁡1=K∧F⁡2=L→BC⊆I⁡F⁡1↔BC⊆I⁡K
13 fveq2 ⊢F⁡2=L→I⁡F⁡2=I⁡L
14 13 sseq2d ⊢F⁡2=L→CD⊆I⁡F⁡2↔CD⊆I⁡L
15 14 3ad2ant3 ⊢F⁡0=J∧F⁡1=K∧F⁡2=L→CD⊆I⁡F⁡2↔CD⊆I⁡L
16 9 12 15 3anbi123d ⊢F⁡0=J∧F⁡1=K∧F⁡2=L→AB⊆I⁡F⁡0∧BC⊆I⁡F⁡1∧CD⊆I⁡F⁡2↔AB⊆I⁡J∧BC⊆I⁡K∧CD⊆I⁡L
17 6 16 syl ⊢φ→AB⊆I⁡F⁡0∧BC⊆I⁡F⁡1∧CD⊆I⁡F⁡2↔AB⊆I⁡J∧BC⊆I⁡K∧CD⊆I⁡L
18 5 17 mpbird ⊢φ→AB⊆I⁡F⁡0∧BC⊆I⁡F⁡1∧CD⊆I⁡F⁡2