Metamath Proof Explorer

Theorem 2wlkdlem6

Description: Lemma 6 for 2wlkd . (Contributed by AV, 23-Jan-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 2wlkdlem6 ⊢φ→B∈I⁡J∧B∈I⁡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 ⊢φ→AB⊆I⁡J∧BC⊆I⁡K
6 prcom ⊢AB=BA
7 6 sseq1i ⊢AB⊆I⁡J↔BA⊆I⁡J
8 7 biimpi ⊢AB⊆I⁡J→BA⊆I⁡J
9 8 adantl ⊢φ∧AB⊆I⁡J→BA⊆I⁡J
10 3 simp2d ⊢φ→B∈V
11 3 simp1d ⊢φ→A∈V
12 11 adantr ⊢φ∧AB⊆I⁡J→A∈V
13 prssg ⊢B∈V∧A∈V→B∈I⁡J∧A∈I⁡J↔BA⊆I⁡J
14 10 12 13 syl2an2r ⊢φ∧AB⊆I⁡J→B∈I⁡J∧A∈I⁡J↔BA⊆I⁡J
15 9 14 mpbird ⊢φ∧AB⊆I⁡J→B∈I⁡J∧A∈I⁡J
16 15 simpld ⊢φ∧AB⊆I⁡J→B∈I⁡J
17 16 ex ⊢φ→AB⊆I⁡J→B∈I⁡J
18 simpr ⊢φ∧BC⊆I⁡K→BC⊆I⁡K
19 3 simp3d ⊢φ→C∈V
20 19 adantr ⊢φ∧BC⊆I⁡K→C∈V
21 prssg ⊢B∈V∧C∈V→B∈I⁡K∧C∈I⁡K↔BC⊆I⁡K
22 10 20 21 syl2an2r ⊢φ∧BC⊆I⁡K→B∈I⁡K∧C∈I⁡K↔BC⊆I⁡K
23 18 22 mpbird ⊢φ∧BC⊆I⁡K→B∈I⁡K∧C∈I⁡K
24 23 simpld ⊢φ∧BC⊆I⁡K→B∈I⁡K
25 24 ex ⊢φ→BC⊆I⁡K→B∈I⁡K
26 17 25 anim12d ⊢φ→AB⊆I⁡J∧BC⊆I⁡K→B∈I⁡J∧B∈I⁡K
27 5 26 mpd ⊢φ→B∈I⁡J∧B∈I⁡K