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 ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩
3wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 𝐿 ”⟩
3wlkd.s ⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) )
3wlkd.n ⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) )
3wlkd.e ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ∧ { 𝐶 , 𝐷 } ⊆ ( 𝐼 ‘ 𝐿 ) ) )
Assertion 3wlkdlem7 ( 𝜑 → ( 𝐽 ∈ V ∧ 𝐾 ∈ V ∧ 𝐿 ∈ V ) )

Proof

Step Hyp Ref Expression
1 3wlkd.p ⊢ 𝑃 = ⟨“ 𝐴 𝐵 𝐶 𝐷 ”⟩
2 3wlkd.f ⊢ 𝐹 = ⟨“ 𝐽 𝐾 𝐿 ”⟩
3 3wlkd.s ⊢ ( 𝜑 → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) )
4 3wlkd.n ⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ) ∧ 𝐶 ≠ 𝐷 ) )
5 3wlkd.e ⊢ ( 𝜑 → ( { 𝐴 , 𝐵 } ⊆ ( 𝐼 ‘ 𝐽 ) ∧ { 𝐵 , 𝐶 } ⊆ ( 𝐼 ‘ 𝐾 ) ∧ { 𝐶 , 𝐷 } ⊆ ( 𝐼 ‘ 𝐿 ) ) )
6 1 2 3 4 5 3wlkdlem6 ⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ∧ 𝐶 ∈ ( 𝐼 ‘ 𝐿 ) ) )
7 elfvex ⊢ ( 𝐴 ∈ ( 𝐼 ‘ 𝐽 ) → 𝐽 ∈ V )
8 elfvex ⊢ ( 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) → 𝐾 ∈ V )
9 elfvex ⊢ ( 𝐶 ∈ ( 𝐼 ‘ 𝐿 ) → 𝐿 ∈ V )
10 7 8 9 3anim123i ⊢ ( ( 𝐴 ∈ ( 𝐼 ‘ 𝐽 ) ∧ 𝐵 ∈ ( 𝐼 ‘ 𝐾 ) ∧ 𝐶 ∈ ( 𝐼 ‘ 𝐿 ) ) → ( 𝐽 ∈ V ∧ 𝐾 ∈ V ∧ 𝐿 ∈ V ) )
11 6 10 syl ⊢ ( 𝜑 → ( 𝐽 ∈ V ∧ 𝐾 ∈ V ∧ 𝐿 ∈ V ) )