Metamath Proof Explorer

Theorem tglnpt4

Description: Find a second point on a line, outside of a second line. (Contributed by Thierry Arnoux, 17-Jun-2026)

Ref Expression
Hypotheses tglnpt2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tglnpt2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglnpt2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglnpt2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tglnpt2.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
tglnpt4.y ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
tglnpt4.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
tglnpt4.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion tglnpt4 ( 𝜑 → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 )

Proof

Step Hyp Ref Expression
1 tglnpt2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tglnpt2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tglnpt2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tglnpt2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 tglnpt2.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6 tglnpt4.y ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
7 tglnpt4.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8 tglnpt4.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
9 4 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → 𝐺 ∈ TarskiG )
10 5 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → 𝐴 ∈ ran 𝐿 )
11 7 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
12 1 2 3 9 10 11 tglnpt2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑧 ∈ 𝐴 𝑋 ≠ 𝑧 )
13 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ∈ 𝐴 )
14 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → 𝑋 ≠ 𝑧 )
15 14 neneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → ¬ 𝑋 = 𝑧 )
16 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐺 ∈ TarskiG )
17 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐴 ∈ ran 𝐿 )
18 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐵 ∈ ran 𝐿 )
19 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐴 ≠ 𝐵 )
20 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 ∈ 𝐴 )
21 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
22 20 21 elind ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 ∈ ( 𝐴 ∩ 𝐵 ) )
23 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐴 )
24 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
25 23 24 elind ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( 𝐴 ∩ 𝐵 ) )
26 1 2 3 16 17 18 19 22 25 tglineineq ⊢ ( ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑋 = 𝑧 )
27 15 26 mtand ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → ¬ 𝑧 ∈ 𝐵 )
28 13 27 eldifd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) )
29 14 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ≠ 𝑋 )
30 28 29 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → ( 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) )
31 30 expl ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑋 ≠ 𝑧 ) → ( 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ) )
32 31 reximdv2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( ∃ 𝑧 ∈ 𝐴 𝑋 ≠ 𝑧 → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 ) )
33 12 32 mpd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 )
34 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐺 ∈ TarskiG )
35 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝐴 ∈ ran 𝐿 )
36 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → 𝑋 ∈ 𝐴 )
37 1 2 3 34 35 36 tglnpt2 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∃ 𝑧 ∈ 𝐴 𝑋 ≠ 𝑧 )
38 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ∈ 𝐴 )
39 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
40 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐴 )
41 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
42 40 41 elind ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( 𝐴 ∩ 𝐵 ) )
43 42 ne0d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
44 43 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) ∧ 𝑧 ∈ 𝐵 ) → ¬ ( 𝐴 ∩ 𝐵 ) = ∅ )
45 39 44 pm2.65da ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → ¬ 𝑧 ∈ 𝐵 )
46 38 45 eldifd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) )
47 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → 𝑋 ≠ 𝑧 )
48 47 necomd ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → 𝑧 ≠ 𝑋 )
49 46 48 jca ⊢ ( ( ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑋 ≠ 𝑧 ) → ( 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) )
50 49 expl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑋 ≠ 𝑧 ) → ( 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ) )
51 50 reximdv2 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ∃ 𝑧 ∈ 𝐴 𝑋 ≠ 𝑧 → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 ) )
52 37 51 mpd ⊢ ( ( 𝜑 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 )
53 52 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 )
54 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
55 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐺 ∈ TarskiG )
56 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝐴 ∈ ran 𝐿 )
57 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑋 ∈ 𝐴 )
58 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) )
59 58 elin1d ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑦 ∈ 𝐴 )
60 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) )
61 60 elin2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
62 61 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
63 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → ¬ 𝑋 ∈ 𝐵 )
64 nelne2 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐵 ) → 𝑦 ≠ 𝑋 )
65 62 63 64 syl2anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑦 ≠ 𝑋 )
66 65 necomd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → 𝑋 ≠ 𝑦 )
67 1 2 3 55 56 57 59 66 tglnpt3 ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑦 ) )
68 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) → 𝑧 ∈ 𝐴 )
69 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) → 𝑧 ≠ 𝑦 )
70 69 neneqd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) → ¬ 𝑧 = 𝑦 )
71 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐺 ∈ TarskiG )
72 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐴 ∈ ran 𝐿 )
73 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐵 ∈ ran 𝐿 )
74 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑧 ∈ 𝐵 ) → 𝐴 ≠ 𝐵 )
75 68 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐴 )
76 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
77 75 76 elind ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ( 𝐴 ∩ 𝐵 ) )
78 60 ad4antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) )
79 1 2 3 71 72 73 74 77 78 tglineineq ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 = 𝑦 )
80 70 79 mtand ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) → ¬ 𝑧 ∈ 𝐵 )
81 68 80 eldifd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) → 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) )
82 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) → 𝑧 ≠ 𝑋 )
83 81 82 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑧 ≠ 𝑋 ) ∧ 𝑧 ≠ 𝑦 ) → ( 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) )
84 83 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) )
85 84 expl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑦 ) ) → ( 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) ∧ 𝑧 ≠ 𝑋 ) ) )
86 85 reximdv2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑦 ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 ) )
87 86 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → ( ∃ 𝑧 ∈ 𝐴 ( 𝑧 ≠ 𝑋 ∧ 𝑧 ≠ 𝑦 ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 ) )
88 67 87 mpd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 )
89 88 adantlr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ 𝑦 ∈ ( 𝐴 ∩ 𝐵 ) ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 )
90 54 89 n0limd ⊢ ( ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 )
91 53 90 pm2.61dane ⊢ ( ( 𝜑 ∧ ¬ 𝑋 ∈ 𝐵 ) → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 )
92 33 91 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( 𝐴 ∖ 𝐵 ) 𝑧 ≠ 𝑋 )