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