Metamath Proof Explorer

Theorem 2wlkdlem9

Description: Lemma 9 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 ⊢φ→AB⊆I⁡J∧BC⊆I⁡K
Assertion 2wlkdlem9 ⊢φ→AB⊆I⁡F⁡0∧BC⊆I⁡F⁡1

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 ⊢φ→AB⊆I⁡J∧BC⊆I⁡K
6 1 2 3 4 5 2wlkdlem8 ⊢φ→F⁡0=J∧F⁡1=K
7 fveq2 ⊢F⁡0=J→I⁡F⁡0=I⁡J
8 7 adantr ⊢F⁡0=J∧F⁡1=K→I⁡F⁡0=I⁡J
9 8 sseq2d ⊢F⁡0=J∧F⁡1=K→AB⊆I⁡F⁡0↔AB⊆I⁡J
10 fveq2 ⊢F⁡1=K→I⁡F⁡1=I⁡K
11 10 adantl ⊢F⁡0=J∧F⁡1=K→I⁡F⁡1=I⁡K
12 11 sseq2d ⊢F⁡0=J∧F⁡1=K→BC⊆I⁡F⁡1↔BC⊆I⁡K
13 9 12 anbi12d ⊢F⁡0=J∧F⁡1=K→AB⊆I⁡F⁡0∧BC⊆I⁡F⁡1↔AB⊆I⁡J∧BC⊆I⁡K
14 6 13 syl ⊢φ→AB⊆I⁡F⁡0∧BC⊆I⁡F⁡1↔AB⊆I⁡J∧BC⊆I⁡K
15 5 14 mpbird ⊢φ→AB⊆I⁡F⁡0∧BC⊆I⁡F⁡1