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 ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ 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 ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
6 prcom ⊢ A B = B A
7 6 sseq1i ⊢ A B ⊆ I ⁡ J ↔ B A ⊆ I ⁡ J
8 7 biimpi ⊢ A B ⊆ I ⁡ J → B A ⊆ I ⁡ J
9 8 adantl ⊢ φ ∧ A B ⊆ I ⁡ J → B A ⊆ I ⁡ J
10 3 simp2d ⊢ φ → B ∈ V
11 3 simp1d ⊢ φ → A ∈ V
12 11 adantr ⊢ φ ∧ A B ⊆ I ⁡ J → A ∈ V
13 prssg ⊢ B ∈ V ∧ A ∈ V → B ∈ I ⁡ J ∧ A ∈ I ⁡ J ↔ B A ⊆ I ⁡ J
14 10 12 13 syl2an2r ⊢ φ ∧ A B ⊆ I ⁡ J → B ∈ I ⁡ J ∧ A ∈ I ⁡ J ↔ B A ⊆ I ⁡ J
15 9 14 mpbird ⊢ φ ∧ A B ⊆ I ⁡ J → B ∈ I ⁡ J ∧ A ∈ I ⁡ J
16 15 simpld ⊢ φ ∧ A B ⊆ I ⁡ J → B ∈ I ⁡ J
17 16 ex ⊢ φ → A B ⊆ I ⁡ J → B ∈ I ⁡ J
18 simpr ⊢ φ ∧ B C ⊆ I ⁡ K → B C ⊆ I ⁡ K
19 3 simp3d ⊢ φ → C ∈ V
20 19 adantr ⊢ φ ∧ B C ⊆ I ⁡ K → C ∈ V
21 prssg ⊢ B ∈ V ∧ C ∈ V → B ∈ I ⁡ K ∧ C ∈ I ⁡ K ↔ B C ⊆ I ⁡ K
22 10 20 21 syl2an2r ⊢ φ ∧ B C ⊆ I ⁡ K → B ∈ I ⁡ K ∧ C ∈ I ⁡ K ↔ B C ⊆ I ⁡ K
23 18 22 mpbird ⊢ φ ∧ B C ⊆ I ⁡ K → B ∈ I ⁡ K ∧ C ∈ I ⁡ K
24 23 simpld ⊢ φ ∧ B C ⊆ I ⁡ K → B ∈ I ⁡ K
25 24 ex ⊢ φ → B C ⊆ I ⁡ K → B ∈ I ⁡ K
26 17 25 anim12d ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K → B ∈ I ⁡ J ∧ B ∈ I ⁡ K
27 5 26 mpd ⊢ φ → B ∈ I ⁡ J ∧ B ∈ I ⁡ K