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

Metamath Proof Explorer

Theorem dvh3dim2

Description: There is a vector that is outside of 2 spans with a common vector. (Contributed by NM, 13-May-2015)

Ref Expression
Hypotheses dvh3dim.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvh3dim.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvh3dim.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dvh3dim.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dvh3dim.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dvh3dim.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
dvh3dim.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
dvh3dim2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
Assertion dvh3dim2 ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )

Proof

Step Hyp Ref Expression
1 dvh3dim.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvh3dim.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dvh3dim.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 dvh3dim.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5 dvh3dim.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 dvh3dim.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7 dvh3dim.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8 dvh3dim2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
9 1 2 3 4 5 6 8 dvh3dim ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
11 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
12 1 2 5 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑧 ∈ 𝑉 ) → 𝑈 ∈ LMod )
14 3 11 4 12 6 8 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑈 ) )
15 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑈 ) )
16 3 4 12 6 8 lspprid1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
17 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑧 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
18 simplr ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑧 ∈ 𝑉 ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
19 11 4 13 15 17 18 lspprss ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑧 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
20 19 ssneld ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑧 ∈ 𝑉 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
21 20 ancrd ⊢ ( ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑧 ∈ 𝑉 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ) )
22 21 reximdva ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ) )
23 10 22 mpd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
24 1 2 3 4 5 6 7 dvh3dim ⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑉 ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ∃ 𝑤 ∈ 𝑉 ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
26 simpl1l ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝜑 )
27 26 12 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑈 ∈ LMod )
28 simpl2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑤 ∈ 𝑉 )
29 26 7 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑌 ∈ 𝑉 )
30 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
31 3 30 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑤 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ 𝑉 )
32 27 28 29 31 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ 𝑉 )
33 3 11 4 12 6 7 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
34 26 33 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
35 3 4 12 6 7 lspprid2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
36 26 35 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
37 simpl3 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
38 3 30 11 27 34 36 28 37 lssvancl2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
39 26 14 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑈 ) )
40 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
41 simpl1r ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
42 3 30 11 27 39 40 29 41 lssvancl1 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
43 eleq1 ⊢ ( 𝑧 = ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
44 43 notbid ⊢ ( 𝑧 = ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
45 eleq1 ⊢ ( 𝑧 = ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
46 45 notbid ⊢ ( 𝑧 = ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
47 44 46 anbi12d ⊢ ( 𝑧 = ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) → ( ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ↔ ( ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ) )
48 47 rspcev ⊢ ( ( ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ 𝑉 ∧ ( ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
49 32 38 42 48 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
50 simpl2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → 𝑤 ∈ 𝑉 )
51 simpl3 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
52 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) )
53 eleq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
54 53 notbid ⊢ ( 𝑧 = 𝑤 → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
55 eleq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
56 55 notbid ⊢ ( 𝑧 = 𝑤 → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ↔ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
57 54 56 anbi12d ⊢ ( 𝑧 = 𝑤 → ( ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ↔ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ) )
58 57 rspcev ⊢ ( ( 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
59 50 51 52 58 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
60 49 59 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
61 60 rexlimdv3a ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ( ∃ 𝑤 ∈ 𝑉 ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) ) )
62 25 61 mpd ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )
63 23 62 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑍 } ) ) )