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

Metamath Proof Explorer

Theorem 3wlkdlem7

Description: Lemma 7 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 3wlkdlem7 ⊢ φ → J ∈ V ∧ K ∈ V ∧ L ∈ V

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 3wlkdlem6 ⊢ φ → A ∈ I ⁡ J ∧ B ∈ I ⁡ K ∧ C ∈ I ⁡ L
7 elfvex ⊢ A ∈ I ⁡ J → J ∈ V
8 elfvex ⊢ B ∈ I ⁡ K → K ∈ V
9 elfvex ⊢ C ∈ I ⁡ L → L ∈ V
10 7 8 9 3anim123i ⊢ A ∈ I ⁡ J ∧ B ∈ I ⁡ K ∧ C ∈ I ⁡ L → J ∈ V ∧ K ∈ V ∧ L ∈ V
11 6 10 syl ⊢ φ → J ∈ V ∧ K ∈ V ∧ L ∈ V