Metamath Proof Explorer

Theorem prlngmolem1

Description: Lemma for prlngmo : Contradiction: Assuming two different parallels B and C having a common point X exist to a line A , the geometry cannot be Euclidean (Contributed by Thierry Arnoux, 5-Jul-2026)

Ref Expression
Hypotheses prlngeu.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
prlngeu.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
prlngeu.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
prlngeu.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
prlngeu.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
prlngeu.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
prlngmolem1.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐵 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐵 ) ) ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ∈ ( 𝑎 𝐼 𝑏 ) ) }
prlngmolem1.q ⊢ 𝑄 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑤 ∈ 𝐴 𝑤 ∈ ( 𝑎 𝐼 𝑏 ) ) }
prlngmolem1.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
prlngmolem1.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
prlngmolem1.c ⊢ ( 𝜑 → 𝐶 ∈ ran 𝐿 )
prlngmolem1.1 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
prlngmolem1.2 ⊢ ( 𝜑 → 𝐴 ∥ 𝐶 )
prlngmolem1.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
prlngmolem1.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
prlngmolem1.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
prlngmolem1.w ⊢ ( 𝜑 → 𝑊 ∈ ( 𝐶 ∖ 𝐵 ) )
prlngmolem1.5 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
prlngmolem1.6 ⊢ ( 𝜑 → 𝑊 𝑂 𝑇 )
Assertion prlngmolem1 ( 𝜑 → ¬ 𝐺 ∈ TarskiGE )

Proof

Step Hyp Ref Expression
1 prlngeu.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 prlngeu.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
3 prlngeu.r ⊢ ∥ = ( parlnG ‘ 𝐺 )
4 prlngeu.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 prlngeu.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
6 prlngeu.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑃 ∖ 𝐴 ) )
7 prlngmolem1.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐵 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐵 ) ) ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ∈ ( 𝑎 𝐼 𝑏 ) ) }
8 prlngmolem1.q ⊢ 𝑄 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐴 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐴 ) ) ∧ ∃ 𝑤 ∈ 𝐴 𝑤 ∈ ( 𝑎 𝐼 𝑏 ) ) }
9 prlngmolem1.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
10 prlngmolem1.b ⊢ ( 𝜑 → 𝐵 ∈ ran 𝐿 )
11 prlngmolem1.c ⊢ ( 𝜑 → 𝐶 ∈ ran 𝐿 )
12 prlngmolem1.1 ⊢ ( 𝜑 → 𝐴 ∥ 𝐵 )
13 prlngmolem1.2 ⊢ ( 𝜑 → 𝐴 ∥ 𝐶 )
14 prlngmolem1.3 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
15 prlngmolem1.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐶 )
16 prlngmolem1.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
17 prlngmolem1.w ⊢ ( 𝜑 → 𝑊 ∈ ( 𝐶 ∖ 𝐵 ) )
18 prlngmolem1.5 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
19 prlngmolem1.6 ⊢ ( 𝜑 → 𝑊 𝑂 𝑇 )
20 4 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝐺 ∈ TarskiG )
21 20 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐺 ∈ TarskiG )
22 21 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝐺 ∈ TarskiG )
23 5 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐴 ∈ ran 𝐿 )
24 23 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝐴 ∈ ran 𝐿 )
25 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑟 ∈ 𝑃 )
26 6 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
27 26 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝑋 ∈ 𝑃 )
28 27 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑋 ∈ 𝑃 )
29 28 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑋 ∈ 𝑃 )
30 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
31 12 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐴 ∥ 𝐵 )
32 31 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝐴 ∥ 𝐵 )
33 6 eldifbd ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝐴 )
34 nelne1 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝐵 ≠ 𝐴 )
35 14 33 34 syl2anc ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
36 35 necomd ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
37 36 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐴 ≠ 𝐵 )
38 37 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝐴 ≠ 𝐵 )
39 10 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝐵 ∈ ran 𝐿 )
40 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝑦 ∈ 𝐵 )
41 1 2 9 20 39 40 tglnpt ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝑦 ∈ 𝑃 )
42 41 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑦 ∈ 𝑃 )
43 42 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑦 ∈ 𝑃 )
44 nelne1 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ ¬ 𝑋 ∈ 𝐴 ) → 𝐶 ≠ 𝐴 )
45 15 33 44 syl2anc ⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
46 45 necomd ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
47 2 3 4 13 46 prlngin0 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐶 ) = ∅ )
48 47 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → ( 𝐴 ∩ 𝐶 ) = ∅ )
49 16 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑇 ∈ 𝐴 )
50 21 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝐺 ∈ TarskiG )
51 17 eldifad ⊢ ( 𝜑 → 𝑊 ∈ 𝐶 )
52 1 2 9 4 11 51 tglnpt ⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
53 52 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝑊 ∈ 𝑃 )
54 53 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑊 ∈ 𝑃 )
55 28 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑋 ∈ 𝑃 )
56 1 2 9 4 5 16 tglnpt ⊢ ( 𝜑 → 𝑇 ∈ 𝑃 )
57 56 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝑇 ∈ 𝑃 )
58 57 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑇 ∈ 𝑃 )
59 17 eldifbd ⊢ ( 𝜑 → ¬ 𝑊 ∈ 𝐵 )
60 nelne2 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ ¬ 𝑊 ∈ 𝐵 ) → 𝑋 ≠ 𝑊 )
61 14 59 60 syl2anc ⊢ ( 𝜑 → 𝑋 ≠ 𝑊 )
62 61 necomd ⊢ ( 𝜑 → 𝑊 ≠ 𝑋 )
63 62 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑊 ≠ 𝑋 )
64 simpr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑋 = 𝑦 )
65 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) )
66 65 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) )
67 64 66 eqeltrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑋 ∈ ( 𝑊 𝐼 𝑇 ) )
68 1 9 2 50 54 55 58 63 67 btwnlng3 ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑇 ∈ ( 𝑊 𝐿 𝑋 ) )
69 1 9 2 4 52 26 62 62 11 51 15 tglinethru ⊢ ( 𝜑 → 𝐶 = ( 𝑊 𝐿 𝑋 ) )
70 69 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝐶 = ( 𝑊 𝐿 𝑋 ) )
71 68 70 eleqtrrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑇 ∈ 𝐶 )
72 49 71 elind ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → 𝑇 ∈ ( 𝐴 ∩ 𝐶 ) )
73 72 ne0d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → ( 𝐴 ∩ 𝐶 ) ≠ ∅ )
74 73 neneqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 = 𝑦 ) → ¬ ( 𝐴 ∩ 𝐶 ) = ∅ )
75 48 74 pm2.65da ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → ¬ 𝑋 = 𝑦 )
76 75 neqned ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑋 ≠ 𝑦 )
77 76 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑋 ≠ 𝑦 )
78 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) )
79 1 9 2 22 29 43 25 77 78 btwnlng3 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑟 ∈ ( 𝑋 𝐿 𝑦 ) )
80 39 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐵 ∈ ran 𝐿 )
81 14 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑋 ∈ 𝐵 )
82 40 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑦 ∈ 𝐵 )
83 1 9 2 21 28 42 76 76 80 81 82 tglinethru ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐵 = ( 𝑋 𝐿 𝑦 ) )
84 83 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝐵 = ( 𝑋 𝐿 𝑦 ) )
85 79 84 eleqtrrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑟 ∈ 𝐵 )
86 81 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑋 ∈ 𝐵 )
87 2 30 3 22 32 38 85 86 prlnghpg ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑟 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 )
88 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑠 ∈ 𝑃 )
89 13 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐴 ∥ 𝐶 )
90 89 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝐴 ∥ 𝐶 )
91 46 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐴 ≠ 𝐶 )
92 91 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝐴 ≠ 𝐶 )
93 15 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑋 ∈ 𝐶 )
94 93 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑋 ∈ 𝐶 )
95 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝑣 ∈ 𝑃 )
96 95 ad3antrrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑣 ∈ 𝑃 )
97 96 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑣 ∈ 𝑃 )
98 simp-4r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑋 ≠ 𝑣 )
99 98 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑋 ≠ 𝑣 )
100 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) )
101 1 9 2 22 29 97 88 99 100 btwnlng3 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑠 ∈ ( 𝑋 𝐿 𝑣 ) )
102 11 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐶 ∈ ran 𝐿 )
103 20 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) → 𝐺 ∈ TarskiG )
104 53 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) → 𝑊 ∈ 𝑃 )
105 27 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) → 𝑋 ∈ 𝑃 )
106 95 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) → 𝑣 ∈ 𝑃 )
107 62 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) → 𝑊 ≠ 𝑋 )
108 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) )
109 108 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) → 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) )
110 1 9 2 103 104 105 106 107 109 btwnlng3 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) → 𝑣 ∈ ( 𝑊 𝐿 𝑋 ) )
111 69 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) → 𝐶 = ( 𝑊 𝐿 𝑋 ) )
112 110 111 eleqtrrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) → 𝑣 ∈ 𝐶 )
113 112 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑣 ∈ 𝐶 )
114 1 9 2 21 28 96 98 98 102 93 113 tglinethru ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐶 = ( 𝑋 𝐿 𝑣 ) )
115 114 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝐶 = ( 𝑋 𝐿 𝑣 ) )
116 101 115 eleqtrrd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑠 ∈ 𝐶 )
117 2 30 3 22 90 92 94 116 prlnghpg ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑋 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑠 )
118 1 9 2 22 24 25 8 29 87 88 117 hpgtr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑟 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑠 )
119 118 3anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) ) → 𝑟 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑠 )
120 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
121 16 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑇 ∈ 𝐴 )
122 121 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑇 ∈ 𝐴 )
123 1 9 2 8 22 24 25 29 87 hpgne1 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → ¬ 𝑟 ∈ 𝐴 )
124 2 30 3 22 90 92 116 94 prlnghpg ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑠 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑋 )
125 1 9 2 8 22 24 88 29 124 hpgne1 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → ¬ 𝑠 ∈ 𝐴 )
126 simpr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) )
127 1 120 9 8 25 88 122 123 125 126 islnoppd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → 𝑟 𝑄 𝑠 )
128 1 9 2 8 22 24 25 88 127 lnoppnhpg ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) → ¬ 𝑟 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑠 )
129 128 3anasss ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) ) → ¬ 𝑟 ( ( hpG ‘ 𝐺 ) ‘ 𝐴 ) 𝑠 )
130 119 129 pm2.65da ⊢ ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑟 ∈ 𝑃 ) ∧ 𝑠 ∈ 𝑃 ) → ¬ ( 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) )
131 130 anasss ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ ( 𝑟 ∈ 𝑃 ∧ 𝑠 ∈ 𝑃 ) ) → ¬ ( 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) )
132 131 ralrimivva ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → ∀ 𝑟 ∈ 𝑃 ∀ 𝑠 ∈ 𝑃 ¬ ( 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) )
133 ralnex2 ⊢ ( ∀ 𝑟 ∈ 𝑃 ∀ 𝑠 ∈ 𝑃 ¬ ( 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) ↔ ¬ ∃ 𝑟 ∈ 𝑃 ∃ 𝑠 ∈ 𝑃 ( 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) )
134 132 133 sylib ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → ¬ ∃ 𝑟 ∈ 𝑃 ∃ 𝑠 ∈ 𝑃 ( 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) )
135 simpr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝐺 ∈ TarskiGE )
136 28 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝑋 ∈ 𝑃 )
137 21 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝐺 ∈ TarskiG )
138 80 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝐵 ∈ ran 𝐿 )
139 82 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝑦 ∈ 𝐵 )
140 1 2 9 137 138 139 tglnpt ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝑦 ∈ 𝑃 )
141 96 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝑣 ∈ 𝑃 )
142 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑧 ∈ 𝑃 )
143 142 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝑧 ∈ 𝑃 )
144 57 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝑇 ∈ 𝑃 )
145 simplr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) )
146 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) )
147 47 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → ( 𝐴 ∩ 𝐶 ) = ∅ )
148 16 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝑇 ∈ 𝐴 )
149 21 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝐺 ∈ TarskiG )
150 104 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝑊 ∈ 𝑃 )
151 42 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝑦 ∈ 𝑃 )
152 57 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝑇 ∈ 𝑃 )
153 59 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → ¬ 𝑊 ∈ 𝐵 )
154 nelne2 ⊢ ( ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑊 ∈ 𝐵 ) → 𝑦 ≠ 𝑊 )
155 82 153 154 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑦 ≠ 𝑊 )
156 155 necomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑊 ≠ 𝑦 )
157 156 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝑊 ≠ 𝑦 )
158 65 ad4antr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) )
159 1 9 2 149 150 151 152 157 158 btwnlng3 ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝑇 ∈ ( 𝑊 𝐿 𝑦 ) )
160 104 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑊 ∈ 𝑃 )
161 81 153 elnelneq2d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → ¬ 𝑋 = 𝑊 )
162 21 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑊 = 𝑣 ) → 𝐺 ∈ TarskiG )
163 160 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑊 = 𝑣 ) → 𝑊 ∈ 𝑃 )
164 28 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑊 = 𝑣 ) → 𝑋 ∈ 𝑃 )
165 109 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑊 = 𝑣 ) → 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) )
166 simpr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑊 = 𝑣 ) → 𝑊 = 𝑣 )
167 166 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑊 = 𝑣 ) → ( 𝑊 𝐼 𝑊 ) = ( 𝑊 𝐼 𝑣 ) )
168 165 167 eleqtrrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑊 = 𝑣 ) → 𝑋 ∈ ( 𝑊 𝐼 𝑊 ) )
169 1 120 9 162 163 164 168 axtgbtwnid ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑊 = 𝑣 ) → 𝑊 = 𝑋 )
170 169 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑊 = 𝑣 ) → 𝑋 = 𝑊 )
171 161 170 mtand ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → ¬ 𝑊 = 𝑣 )
172 171 neqned ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑊 ≠ 𝑣 )
173 51 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑊 ∈ 𝐶 )
174 1 9 2 21 160 96 172 172 102 173 113 tglinethru ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝐶 = ( 𝑊 𝐿 𝑣 ) )
175 174 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝐶 = ( 𝑊 𝐿 𝑣 ) )
176 simpr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝑦 = 𝑣 )
177 176 oveq2d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → ( 𝑊 𝐿 𝑦 ) = ( 𝑊 𝐿 𝑣 ) )
178 175 177 eqtr4d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝐶 = ( 𝑊 𝐿 𝑦 ) )
179 159 178 eleqtrrd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝑇 ∈ 𝐶 )
180 148 179 elind ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → 𝑇 ∈ ( 𝐴 ∩ 𝐶 ) )
181 180 ne0d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → ( 𝐴 ∩ 𝐶 ) ≠ ∅ )
182 181 neneqd ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑦 = 𝑣 ) → ¬ ( 𝐴 ∩ 𝐶 ) = ∅ )
183 147 182 pm2.65da ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → ¬ 𝑦 = 𝑣 )
184 183 neqned ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑦 ≠ 𝑣 )
185 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) )
186 1 9 2 21 42 96 142 184 185 btwnlng1 ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑧 ∈ ( 𝑦 𝐿 𝑣 ) )
187 18 neneqd ⊢ ( 𝜑 → ¬ 𝐵 = 𝐶 )
188 187 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → ¬ 𝐵 = 𝐶 )
189 21 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝐺 ∈ TarskiG )
190 28 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝑋 ∈ 𝑃 )
191 96 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝑣 ∈ 𝑃 )
192 98 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝑋 ≠ 𝑣 )
193 42 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝑦 ∈ 𝑃 )
194 76 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝑋 ≠ 𝑦 )
195 1 9 2 189 190 193 194 tgelrnln ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → ( 𝑋 𝐿 𝑦 ) ∈ ran 𝐿 )
196 1 9 2 189 190 193 194 tglinerflx1 ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝑋 ∈ ( 𝑋 𝐿 𝑦 ) )
197 simpr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) )
198 184 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝑦 ≠ 𝑣 )
199 1 9 2 189 190 193 191 194 197 198 lnrot2 ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝑣 ∈ ( 𝑋 𝐿 𝑦 ) )
200 1 9 2 189 190 191 192 192 195 196 199 tglinethru ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → ( 𝑋 𝐿 𝑦 ) = ( 𝑋 𝐿 𝑣 ) )
201 83 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝐵 = ( 𝑋 𝐿 𝑦 ) )
202 114 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝐶 = ( 𝑋 𝐿 𝑣 ) )
203 200 201 202 3eqtr4d ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝐵 = 𝐶 )
204 188 203 mtand ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → ¬ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) )
205 nelne2 ⊢ ( ( 𝑧 ∈ ( 𝑦 𝐿 𝑣 ) ∧ ¬ 𝑋 ∈ ( 𝑦 𝐿 𝑣 ) ) → 𝑧 ≠ 𝑋 )
206 186 204 205 syl2anc ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑧 ≠ 𝑋 )
207 206 necomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → 𝑋 ≠ 𝑧 )
208 207 adantr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → 𝑋 ≠ 𝑧 )
209 1 120 9 135 136 140 141 143 144 145 146 208 axtgeucl ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ∧ 𝐺 ∈ TarskiGE ) → ∃ 𝑟 ∈ 𝑃 ∃ 𝑠 ∈ 𝑃 ( 𝑦 ∈ ( 𝑋 𝐼 𝑟 ) ∧ 𝑣 ∈ ( 𝑋 𝐼 𝑠 ) ∧ 𝑇 ∈ ( 𝑟 𝐼 𝑠 ) ) )
210 134 209 mtand ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) → ¬ 𝐺 ∈ TarskiGE )
211 210 anasss ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) ) → ¬ 𝐺 ∈ TarskiGE )
212 1 120 9 20 53 41 57 65 tgbtwncom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝑦 ∈ ( 𝑇 𝐼 𝑊 ) )
213 1 120 9 20 53 27 95 108 tgbtwncom ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → 𝑋 ∈ ( 𝑣 𝐼 𝑊 ) )
214 1 120 9 20 57 95 53 41 27 212 213 axtgpasch ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → ∃ 𝑧 ∈ 𝑃 ( 𝑧 ∈ ( 𝑦 𝐼 𝑣 ) ∧ 𝑧 ∈ ( 𝑋 𝐼 𝑇 ) ) )
215 211 214 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ) ∧ 𝑋 ≠ 𝑣 ) → ¬ 𝐺 ∈ TarskiGE )
216 215 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ∧ 𝑋 ≠ 𝑣 ) ) → ¬ 𝐺 ∈ TarskiGE )
217 1 fvexi ⊢ 𝑃 ∈ V
218 217 a1i ⊢ ( 𝜑 → 𝑃 ∈ V )
219 218 26 52 61 nehash2 ⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ 𝑃 ) )
220 1 120 9 4 52 26 219 tgbtwndiff ⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ∧ 𝑋 ≠ 𝑣 ) )
221 220 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) → ∃ 𝑣 ∈ 𝑃 ( 𝑋 ∈ ( 𝑊 𝐼 𝑣 ) ∧ 𝑋 ≠ 𝑣 ) )
222 216 221 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) → ¬ 𝐺 ∈ TarskiGE )
223 1 120 9 7 52 56 islnopp ⊢ ( 𝜑 → ( 𝑊 𝑂 𝑇 ↔ ( ( ¬ 𝑊 ∈ 𝐵 ∧ ¬ 𝑇 ∈ 𝐵 ) ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) ) )
224 19 223 mpbid ⊢ ( 𝜑 → ( ( ¬ 𝑊 ∈ 𝐵 ∧ ¬ 𝑇 ∈ 𝐵 ) ∧ ∃ 𝑦 ∈ 𝐵 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) ) )
225 224 simprd ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝑦 ∈ ( 𝑊 𝐼 𝑇 ) )
226 222 225 r19.29a ⊢ ( 𝜑 → ¬ 𝐺 ∈ TarskiGE )