Theorem inaghl 29369

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

Hypotheses

Ref	Expression
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

Ref	Expression
inaghl	⊢ (𝜑 → 𝑌(inA‘𝐺)⟨“𝐷𝐵𝐹”⟩)

Proof of Theorem inaghl

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1569   ∈ wcel 2144   ≠ wne 2955  ∃wrex 3086   class class class wbr 5102  ‘cfv 6538  (class class class)co 7420  ⟨“cs3 14997  Basecbs 17392  distcds 17442  TarskiGcstrkg 28894  Itvcitv 28900  hlGchlg 29068  inAcinag 29359

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11259  ax-resscn 11260  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-addrcl 11264  ax-mulcl 11265  ax-mulrcl 11266  ax-mulcom 11267  ax-addass 11268  ax-mulass 11269  ax-distr 11270  ax-i2m1 11271  ax-1ne0 11272  ax-1rid 11273  ax-rnegex 11274  ax-rrecex 11275  ax-cnre 11276  ax-pre-lttri 11277  ax-pre-lttrn 11278  ax-pre-ltadd 11279  ax-pre-mulgt0 11280

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-pss 4014  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-uni 4867  df-int 4907  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7377  df-ov 7423  df-oprab 7424  df-mpo 7425  df-om 7878  df-1st 8001  df-2nd 8002  df-frecs 8302  df-wrecs 8333  df-recs 8382  df-rdg 8421  df-1o 8479  df-oadd 8483  df-er 8720  df-map 8852  df-pm 8853  df-en 8977  df-dom 8978  df-sdom 8979  df-fin 8980  df-dju 9985  df-card 10023  df-pnf 11348  df-mnf 11349  df-xr 11350  df-ltxr 11351  df-le 11352  df-sub 11546  df-neg 11547  df-nn 12339  df-2 12408  df-3 12409  df-n0 12610  df-xnn0 12683  df-z 12697  df-uz 12969  df-fz 13643  df-fzo 13792  df-hash 14478  df-word 14662  df-concat 14719  df-s1 14746  df-s2 15003  df-s3 15004  df-trkgc 28915  df-trkgb 28916  df-trkgcb 28917  df-trkgld 28919  df-trkg 28920  df-cgrg 28979  df-leg 29051  df-hlg 29069  df-mir 29130  df-rag 29174  df-perpg 29176  df-inag 29361

This theorem is used by:  inagcgratrgmain  33059  tgextalem1inag  33075