This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
Assertion 2wlkdlem9 ⊢ φ → A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ 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 ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ 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 → A B ⊆ I ⁡ F ⁡ 0 ↔ A B ⊆ 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 → B C ⊆ I ⁡ F ⁡ 1 ↔ B C ⊆ I ⁡ K
13 9 12 anbi12d ⊢ F ⁡ 0 = J ∧ F ⁡ 1 = K → A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1 ↔ A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
14 6 13 syl ⊢ φ → A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1 ↔ A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K
15 5 14 mpbird ⊢ φ → A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1