Metamath Proof Explorer

Theorem 3wlkdlem9

Description: Lemma 9 for 3wlkd . (Contributed by AV, 7-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p ⊢ P = ⟨“ ABCD ”⟩
3wlkd.f ⊢ F = ⟨“ JKL ”⟩
3wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V
3wlkd.n ⊢ φ → A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D
3wlkd.e ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K ∧ C D ⊆ I ⁡ L
Assertion 3wlkdlem9 ⊢ φ → A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1 ∧ C D ⊆ I ⁡ F ⁡ 2

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢ P = ⟨“ ABCD ”⟩
2 3wlkd.f ⊢ F = ⟨“ JKL ”⟩
3 3wlkd.s ⊢ φ → A ∈ V ∧ B ∈ V ∧ C ∈ V ∧ D ∈ V
4 3wlkd.n ⊢ φ → A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ B ≠ D ∧ C ≠ D
5 3wlkd.e ⊢ φ → A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K ∧ C D ⊆ I ⁡ L
6 1 2 3 4 5 3wlkdlem8 ⊢ φ → F ⁡ 0 = J ∧ F ⁡ 1 = K ∧ F ⁡ 2 = L
7 fveq2 ⊢ F ⁡ 0 = J → I ⁡ F ⁡ 0 = I ⁡ J
8 7 sseq2d ⊢ F ⁡ 0 = J → A B ⊆ I ⁡ F ⁡ 0 ↔ A B ⊆ I ⁡ J
9 8 3ad2ant1 ⊢ F ⁡ 0 = J ∧ F ⁡ 1 = K ∧ F ⁡ 2 = L → A B ⊆ I ⁡ F ⁡ 0 ↔ A B ⊆ I ⁡ J
10 fveq2 ⊢ F ⁡ 1 = K → I ⁡ F ⁡ 1 = I ⁡ K
11 10 sseq2d ⊢ F ⁡ 1 = K → B C ⊆ I ⁡ F ⁡ 1 ↔ B C ⊆ I ⁡ K
12 11 3ad2ant2 ⊢ F ⁡ 0 = J ∧ F ⁡ 1 = K ∧ F ⁡ 2 = L → B C ⊆ I ⁡ F ⁡ 1 ↔ B C ⊆ I ⁡ K
13 fveq2 ⊢ F ⁡ 2 = L → I ⁡ F ⁡ 2 = I ⁡ L
14 13 sseq2d ⊢ F ⁡ 2 = L → C D ⊆ I ⁡ F ⁡ 2 ↔ C D ⊆ I ⁡ L
15 14 3ad2ant3 ⊢ F ⁡ 0 = J ∧ F ⁡ 1 = K ∧ F ⁡ 2 = L → C D ⊆ I ⁡ F ⁡ 2 ↔ C D ⊆ I ⁡ L
16 9 12 15 3anbi123d ⊢ F ⁡ 0 = J ∧ F ⁡ 1 = K ∧ F ⁡ 2 = L → A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1 ∧ C D ⊆ I ⁡ F ⁡ 2 ↔ A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K ∧ C D ⊆ I ⁡ L
17 6 16 syl ⊢ φ → A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1 ∧ C D ⊆ I ⁡ F ⁡ 2 ↔ A B ⊆ I ⁡ J ∧ B C ⊆ I ⁡ K ∧ C D ⊆ I ⁡ L
18 5 17 mpbird ⊢ φ → A B ⊆ I ⁡ F ⁡ 0 ∧ B C ⊆ I ⁡ F ⁡ 1 ∧ C D ⊆ I ⁡ F ⁡ 2