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

Metamath Proof Explorer

Theorem 2wlkdlem7

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

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 2wlkdlem6 ⊢ φ → B ∈ I ⁡ J ∧ B ∈ I ⁡ K
7 elfvex ⊢ B ∈ I ⁡ J → J ∈ V
8 elfvex ⊢ B ∈ I ⁡ K → K ∈ V
9 7 8 anim12i ⊢ B ∈ I ⁡ J ∧ B ∈ I ⁡ K → J ∈ V ∧ K ∈ V
10 6 9 syl ⊢ φ → J ∈ V ∧ K ∈ V