Metamath Proof Explorer

Theorem inaghl

Description: The "point lie in angle" relation is independent of the points chosen on the half lines starting from B . Theorem 11.25 of Schwabhauser p. 101. (Contributed by Thierry Arnoux, 27-Sep-2020)

Ref Expression
Hypotheses isinag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isinag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isinag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
isinag.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
isinag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
isinag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
isinag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
inagflat.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
inagswap.1 ⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
inaghl.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
inaghl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
inaghl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
inaghl.1 ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐵 ) 𝐴 )
inaghl.2 ⊢ ( 𝜑 → 𝐹 ( 𝐾 ‘ 𝐵 ) 𝐶 )
inaghl.3 ⊢ ( 𝜑 → 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑋 )
Assertion inaghl ( 𝜑 → 𝑌 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝐹 ”⟩ )

Proof

Step Hyp Ref Expression
1 isinag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isinag.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 isinag.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 isinag.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
5 isinag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 isinag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 isinag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 inagflat.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
9 inagswap.1 ⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
10 inaghl.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
11 inaghl.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
12 inaghl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
13 inaghl.1 ⊢ ( 𝜑 → 𝐷 ( 𝐾 ‘ 𝐵 ) 𝐴 )
14 inaghl.2 ⊢ ( 𝜑 → 𝐹 ( 𝐾 ‘ 𝐵 ) 𝐶 )
15 inaghl.3 ⊢ ( 𝜑 → 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑋 )
16 1 2 3 10 5 6 8 13 hlne1 ⊢ ( 𝜑 → 𝐷 ≠ 𝐵 )
17 1 2 3 11 7 6 8 14 hlne1 ⊢ ( 𝜑 → 𝐹 ≠ 𝐵 )
18 1 2 3 12 4 6 8 15 hlne1 ⊢ ( 𝜑 → 𝑌 ≠ 𝐵 )
19 16 17 18 3jca ⊢ ( 𝜑 → ( 𝐷 ≠ 𝐵 ∧ 𝐹 ≠ 𝐵 ∧ 𝑌 ≠ 𝐵 ) )
20 6 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ 𝑃 )
21 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ↔ 𝐵 ∈ ( 𝐷 𝐼 𝐹 ) ) )
22 eqeq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 = 𝐵 ↔ 𝐵 = 𝐵 ) )
23 breq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ↔ 𝐵 ( 𝐾 ‘ 𝐵 ) 𝑌 ) )
24 22 23 orbi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ↔ ( 𝐵 = 𝐵 ∨ 𝐵 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
25 21 24 anbi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) ↔ ( 𝐵 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝐵 = 𝐵 ∨ 𝐵 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) ) )
26 25 adantl ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑦 = 𝐵 ) → ( ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) ↔ ( 𝐵 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝐵 = 𝐵 ∨ 𝐵 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) ) )
27 5 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐴 ∈ 𝑃 )
28 10 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐷 ∈ 𝑃 )
29 11 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐹 ∈ 𝑃 )
30 8 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐺 ∈ TarskiG )
31 1 2 3 10 5 6 8 13 hlcomd ⊢ ( 𝜑 → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 )
33 eqid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 )
34 7 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐶 ∈ 𝑃 )
35 1 2 3 11 7 6 8 14 hlcomd ⊢ ( 𝜑 → 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐹 )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐹 )
37 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
38 1 33 2 30 27 20 34 37 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
39 1 2 3 34 29 27 30 20 36 38 btwnhl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐹 𝐼 𝐴 ) )
40 1 33 2 30 29 20 27 39 tgbtwncom ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐴 𝐼 𝐹 ) )
41 1 2 3 27 28 29 30 20 32 40 btwnhl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 ∈ ( 𝐷 𝐼 𝐹 ) )
42 eqidd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → 𝐵 = 𝐵 )
43 42 orcd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐵 = 𝐵 ∨ 𝐵 ( 𝐾 ‘ 𝐵 ) 𝑌 ) )
44 41 43 jca ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ( 𝐵 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝐵 = 𝐵 ∨ 𝐵 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
45 20 26 44 rspcedvd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
46 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ 𝑃 )
47 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
48 47 eleq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) ∧ 𝑦 = 𝑥 ) → ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ↔ 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ) )
49 47 eqeq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) ∧ 𝑦 = 𝑥 ) → ( 𝑦 = 𝐵 ↔ 𝑥 = 𝐵 ) )
50 47 breq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) ∧ 𝑦 = 𝑥 ) → ( 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ↔ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑌 ) )
51 49 50 orbi12d ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) ∧ 𝑦 = 𝑥 ) → ( ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ↔ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
52 48 51 anbi12d ⊢ ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) ∧ 𝑦 = 𝑥 ) → ( ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) ↔ ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) ) )
53 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝑥 = 𝐵 )
54 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐴 ∈ 𝑃 )
55 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐷 ∈ 𝑃 )
56 11 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐹 ∈ 𝑃 )
57 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐺 ∈ TarskiG )
58 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ 𝑃 )
59 31 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 )
60 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐶 ∈ 𝑃 )
61 35 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐹 )
62 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) )
63 1 33 2 57 54 46 60 62 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐶 𝐼 𝐴 ) )
64 53 63 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ ( 𝐶 𝐼 𝐴 ) )
65 1 2 3 60 56 54 57 58 61 64 btwnhl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ ( 𝐹 𝐼 𝐴 ) )
66 1 33 2 57 56 58 54 65 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ ( 𝐴 𝐼 𝐹 ) )
67 1 2 3 54 55 56 57 58 59 66 btwnhl ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝐵 ∈ ( 𝐷 𝐼 𝐹 ) )
68 53 67 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) )
69 53 orcd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑌 ) )
70 68 69 jca ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → ( 𝑥 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
71 46 52 70 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 = 𝐵 ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
72 8 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝐺 ∈ TarskiG )
73 72 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝐺 ∈ TarskiG )
74 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝑧 ∈ 𝑃 )
75 6 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝐵 ∈ 𝑃 )
76 75 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝐵 ∈ 𝑃 )
77 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝐶 ∈ 𝑃 )
78 77 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝐶 ∈ 𝑃 )
79 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝐷 ∈ 𝑃 )
80 79 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝐷 ∈ 𝑃 )
81 11 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝐹 ∈ 𝑃 )
82 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝑥 ∈ 𝑃 )
83 82 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝑥 ∈ 𝑃 )
84 simprl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 )
85 1 2 3 83 74 76 73 84 hlne2 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝑧 ≠ 𝐵 )
86 35 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝐶 ( 𝐾 ‘ 𝐵 ) 𝐹 )
87 simprr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) )
88 1 33 2 73 78 74 80 87 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → 𝑧 ∈ ( 𝐷 𝐼 𝐶 ) )
89 1 2 3 73 74 76 78 80 81 85 86 88 hlpasch ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) )
90 simprr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) )
91 simplr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑦 ∈ 𝑃 )
92 74 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑧 ∈ 𝑃 )
93 12 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑌 ∈ 𝑃 )
94 73 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝐺 ∈ TarskiG )
95 76 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝐵 ∈ 𝑃 )
96 simprl ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 )
97 1 2 3 92 91 95 94 96 hlcomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑧 )
98 82 ad4antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑥 ∈ 𝑃 )
99 4 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑋 ∈ 𝑃 )
100 15 ad8antr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑋 )
101 simp-5r ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 )
102 1 2 3 98 99 95 94 101 hlcomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑋 ( 𝐾 ‘ 𝐵 ) 𝑥 )
103 1 2 3 93 99 98 94 95 100 102 hltr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑥 )
104 simpllr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) )
105 104 simpld ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 )
106 1 2 3 93 98 92 94 95 103 105 hltr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑌 ( 𝐾 ‘ 𝐵 ) 𝑧 )
107 1 2 3 93 92 95 94 106 hlcomd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑌 )
108 1 2 3 91 92 93 94 95 97 107 hltr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 )
109 108 olcd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) )
110 90 109 jca ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) ) → ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
111 110 ex ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) ∧ 𝑦 ∈ 𝑃 ) → ( ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) → ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) ) )
112 111 reximdva ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → ( ∃ 𝑦 ∈ 𝑃 ( 𝑧 ( 𝐾 ‘ 𝐵 ) 𝑦 ∧ 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) ) )
113 89 112 mpd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
114 5 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝐴 ∈ 𝑃 )
115 4 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝑋 ∈ 𝑃 )
116 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 )
117 1 2 3 82 115 75 72 116 hlne1 ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝑥 ≠ 𝐵 )
118 31 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝐴 ( 𝐾 ‘ 𝐵 ) 𝐷 )
119 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) )
120 1 33 2 72 114 82 77 119 tgbtwncom ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → 𝑥 ∈ ( 𝐶 𝐼 𝐴 ) )
121 1 2 3 72 82 75 114 77 79 117 118 120 hlpasch ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → ∃ 𝑧 ∈ 𝑃 ( 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑧 ∧ 𝑧 ∈ ( 𝐶 𝐼 𝐷 ) ) )
122 113 121 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
123 71 122 jaodan ⊢ ( ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
124 123 anasss ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
125 1 2 3 4 5 6 7 8 isinag ⊢ ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) ) )
126 9 125 mpbid ⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐵 ∧ 𝑋 ≠ 𝐵 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) ) )
127 126 simprd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) )
128 127 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵 ∨ 𝑥 ( 𝐾 ‘ 𝐵 ) 𝑋 ) ) )
129 124 128 r19.29a ⊢ ( ( 𝜑 ∧ ¬ 𝐵 ∈ ( 𝐴 𝐼 𝐶 ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
130 45 129 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) )
131 1 2 3 12 10 6 11 8 isinag ⊢ ( 𝜑 → ( 𝑌 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝐹 ”⟩ ↔ ( ( 𝐷 ≠ 𝐵 ∧ 𝐹 ≠ 𝐵 ∧ 𝑌 ≠ 𝐵 ) ∧ ∃ 𝑦 ∈ 𝑃 ( 𝑦 ∈ ( 𝐷 𝐼 𝐹 ) ∧ ( 𝑦 = 𝐵 ∨ 𝑦 ( 𝐾 ‘ 𝐵 ) 𝑌 ) ) ) ) )
132 19 130 131 mpbir2and ⊢ ( 𝜑 → 𝑌 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐵 𝐹 ”⟩ )