Metamath Proof Explorer

Theorem colline

Description: Three points are colinear iff there is a line through all three of them. Theorem 6.23 of Schwabhauser p. 46. (Contributed by Thierry Arnoux, 28-May-2019)

Ref Expression
Hypotheses tglineintmo.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tglineintmo.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tglineintmo.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tglineintmo.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
colline.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
colline.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
colline.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
colline.4 ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
Assertion colline ( 𝜑 → ( ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ↔ ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) )

Proof

Step Hyp Ref Expression
1 tglineintmo.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tglineintmo.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 tglineintmo.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 tglineintmo.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 colline.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
6 colline.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
7 colline.3 ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
8 colline.4 ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
9 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → 𝐺 ∈ TarskiG )
10 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → 𝑋 ∈ 𝑃 )
11 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → 𝑥 ∈ 𝑃 )
12 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → 𝑋 ≠ 𝑥 )
13 1 2 3 9 10 11 12 tgelrnln ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → ( 𝑋 𝐿 𝑥 ) ∈ ran 𝐿 )
14 1 2 3 9 10 11 12 tglinerflx1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → 𝑋 ∈ ( 𝑋 𝐿 𝑥 ) )
15 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → 𝑌 = 𝑍 )
16 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → 𝑋 = 𝑍 )
17 16 14 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → 𝑍 ∈ ( 𝑋 𝐿 𝑥 ) )
18 15 17 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → 𝑌 ∈ ( 𝑋 𝐿 𝑥 ) )
19 eleq2 ⊢ ( 𝑎 = ( 𝑋 𝐿 𝑥 ) → ( 𝑋 ∈ 𝑎 ↔ 𝑋 ∈ ( 𝑋 𝐿 𝑥 ) ) )
20 eleq2 ⊢ ( 𝑎 = ( 𝑋 𝐿 𝑥 ) → ( 𝑌 ∈ 𝑎 ↔ 𝑌 ∈ ( 𝑋 𝐿 𝑥 ) ) )
21 eleq2 ⊢ ( 𝑎 = ( 𝑋 𝐿 𝑥 ) → ( 𝑍 ∈ 𝑎 ↔ 𝑍 ∈ ( 𝑋 𝐿 𝑥 ) ) )
22 19 20 21 3anbi123d ⊢ ( 𝑎 = ( 𝑋 𝐿 𝑥 ) → ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ↔ ( 𝑋 ∈ ( 𝑋 𝐿 𝑥 ) ∧ 𝑌 ∈ ( 𝑋 𝐿 𝑥 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑥 ) ) ) )
23 22 rspcev ⊢ ( ( ( 𝑋 𝐿 𝑥 ) ∈ ran 𝐿 ∧ ( 𝑋 ∈ ( 𝑋 𝐿 𝑥 ) ∧ 𝑌 ∈ ( 𝑋 𝐿 𝑥 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑥 ) ) ) → ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) )
24 13 14 18 17 23 syl13anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑋 ≠ 𝑥 ) → ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) )
25 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
26 1 25 2 4 8 5 tglowdim1i ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 𝑋 ≠ 𝑥 )
27 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) → ∃ 𝑥 ∈ 𝑃 𝑋 ≠ 𝑥 )
28 24 27 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 = 𝑍 ) → ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) )
29 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 ≠ 𝑍 ) → 𝐺 ∈ TarskiG )
30 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 ≠ 𝑍 ) → 𝑋 ∈ 𝑃 )
31 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 ≠ 𝑍 ) → 𝑍 ∈ 𝑃 )
32 simpr ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 ≠ 𝑍 ) → 𝑋 ≠ 𝑍 )
33 1 2 3 29 30 31 32 tgelrnln ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 ≠ 𝑍 ) → ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 )
34 1 2 3 29 30 31 32 tglinerflx1 ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 ≠ 𝑍 ) → 𝑋 ∈ ( 𝑋 𝐿 𝑍 ) )
35 simplr ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 ≠ 𝑍 ) → 𝑌 = 𝑍 )
36 1 2 3 29 30 31 32 tglinerflx2 ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 ≠ 𝑍 ) → 𝑍 ∈ ( 𝑋 𝐿 𝑍 ) )
37 35 36 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 ≠ 𝑍 ) → 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) )
38 eleq2 ⊢ ( 𝑎 = ( 𝑋 𝐿 𝑍 ) → ( 𝑋 ∈ 𝑎 ↔ 𝑋 ∈ ( 𝑋 𝐿 𝑍 ) ) )
39 eleq2 ⊢ ( 𝑎 = ( 𝑋 𝐿 𝑍 ) → ( 𝑌 ∈ 𝑎 ↔ 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ) )
40 eleq2 ⊢ ( 𝑎 = ( 𝑋 𝐿 𝑍 ) → ( 𝑍 ∈ 𝑎 ↔ 𝑍 ∈ ( 𝑋 𝐿 𝑍 ) ) )
41 38 39 40 3anbi123d ⊢ ( 𝑎 = ( 𝑋 𝐿 𝑍 ) → ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ↔ ( 𝑋 ∈ ( 𝑋 𝐿 𝑍 ) ∧ 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑍 ) ) ) )
42 41 rspcev ⊢ ( ( ( 𝑋 𝐿 𝑍 ) ∈ ran 𝐿 ∧ ( 𝑋 ∈ ( 𝑋 𝐿 𝑍 ) ∧ 𝑌 ∈ ( 𝑋 𝐿 𝑍 ) ∧ 𝑍 ∈ ( 𝑋 𝐿 𝑍 ) ) ) → ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) )
43 33 34 37 36 42 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝑌 = 𝑍 ) ∧ 𝑋 ≠ 𝑍 ) → ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) )
44 28 43 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑌 = 𝑍 ) → ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) )
45 44 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) ∧ 𝑌 = 𝑍 ) → ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) )
46 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝜑 )
47 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑌 ≠ 𝑍 )
48 47 neneqd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → ¬ 𝑌 = 𝑍 )
49 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
50 orel2 ⊢ ( ¬ 𝑌 = 𝑍 → ( ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) )
51 48 49 50 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
52 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝐺 ∈ TarskiG )
53 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑌 ∈ 𝑃 )
54 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑍 ∈ 𝑃 )
55 simpr ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑌 ≠ 𝑍 )
56 1 2 3 52 53 54 55 tgelrnln ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
57 46 51 47 56 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 )
58 1 2 3 52 53 54 55 tglinerflx1 ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑌 ∈ ( 𝑌 𝐿 𝑍 ) )
59 46 51 47 58 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑌 ∈ ( 𝑌 𝐿 𝑍 ) )
60 1 2 3 52 53 54 55 tglinerflx2 ⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑍 ∈ ( 𝑌 𝐿 𝑍 ) )
61 46 51 47 60 syl21anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑍 ∈ ( 𝑌 𝐿 𝑍 ) )
62 eleq2 ⊢ ( 𝑎 = ( 𝑌 𝐿 𝑍 ) → ( 𝑋 ∈ 𝑎 ↔ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) )
63 eleq2 ⊢ ( 𝑎 = ( 𝑌 𝐿 𝑍 ) → ( 𝑌 ∈ 𝑎 ↔ 𝑌 ∈ ( 𝑌 𝐿 𝑍 ) ) )
64 eleq2 ⊢ ( 𝑎 = ( 𝑌 𝐿 𝑍 ) → ( 𝑍 ∈ 𝑎 ↔ 𝑍 ∈ ( 𝑌 𝐿 𝑍 ) ) )
65 62 63 64 3anbi123d ⊢ ( 𝑎 = ( 𝑌 𝐿 𝑍 ) → ( ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ↔ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∧ 𝑌 ∈ ( 𝑌 𝐿 𝑍 ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑍 ) ) ) )
66 65 rspcev ⊢ ( ( ( 𝑌 𝐿 𝑍 ) ∈ ran 𝐿 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∧ 𝑌 ∈ ( 𝑌 𝐿 𝑍 ) ∧ 𝑍 ∈ ( 𝑌 𝐿 𝑍 ) ) ) → ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) )
67 57 51 59 61 66 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) ∧ 𝑌 ≠ 𝑍 ) → ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) )
68 45 67 pm2.61dane ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ) → ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) )
69 df-ne ⊢ ( 𝑌 ≠ 𝑍 ↔ ¬ 𝑌 = 𝑍 )
70 simplr1 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑋 ∈ 𝑎 )
71 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝐺 ∈ TarskiG )
72 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑌 ∈ 𝑃 )
73 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑍 ∈ 𝑃 )
74 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑌 ≠ 𝑍 )
75 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑎 ∈ ran 𝐿 )
76 simplr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑌 ∈ 𝑎 )
77 simplr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑍 ∈ 𝑎 )
78 1 2 3 71 72 73 74 74 75 76 77 tglinethru ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑎 = ( 𝑌 𝐿 𝑍 ) )
79 70 78 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) ∧ 𝑌 ≠ 𝑍 ) → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) )
80 79 ex ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) → ( 𝑌 ≠ 𝑍 → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) )
81 69 80 biimtrrid ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) → ( ¬ 𝑌 = 𝑍 → 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) )
82 81 orrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) → ( 𝑌 = 𝑍 ∨ 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ) )
83 82 orcomd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ran 𝐿 ) ∧ ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) → ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
84 83 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) → ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) )
85 68 84 impbida ⊢ ( 𝜑 → ( ( 𝑋 ∈ ( 𝑌 𝐿 𝑍 ) ∨ 𝑌 = 𝑍 ) ↔ ∃ 𝑎 ∈ ran 𝐿 ( 𝑋 ∈ 𝑎 ∧ 𝑌 ∈ 𝑎 ∧ 𝑍 ∈ 𝑎 ) ) )