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	$⊢ P = {Base}_{G}$
	isinag.i	$⊢ I = Itv (G)$
	isinag.k	$⊢ K = {hl}_{𝒢} (G)$
	isinag.x	$⊢ φ \to X \in P$
	isinag.a	$⊢ φ \to A \in P$
	isinag.b	$⊢ φ \to B \in P$
	isinag.c	$⊢ φ \to C \in P$
	inagflat.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	inagswap.1	$⊢ φ \to X \in_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
	inaghl.d	$⊢ φ \to D \in P$
	inaghl.f	$⊢ φ \to F \in P$
	inaghl.y	$⊢ φ \to Y \in P$
	inaghl.1	$⊢ φ \to D K (B) A$
	inaghl.2	$⊢ φ \to F K (B) C$
	inaghl.3	$⊢ φ \to Y K (B) X$
Assertion	inaghl	$⊢ φ \to Y \in_{𝒢}^{∠} (G) ⟨“ D B F ”⟩$

Proof

Step	Hyp	Ref	Expression
1		isinag.p	$⊢ P = {Base}_{G}$
2		isinag.i	$⊢ I = Itv (G)$
3		isinag.k	$⊢ K = {hl}_{𝒢} (G)$
4		isinag.x	$⊢ φ \to X \in P$
5		isinag.a	$⊢ φ \to A \in P$
6		isinag.b	$⊢ φ \to B \in P$
7		isinag.c	$⊢ φ \to C \in P$
8		inagflat.g	$⊢ φ \to G \in 𝒢_{Tarski}$
9		inagswap.1	$⊢ φ \to X \in_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
10		inaghl.d	$⊢ φ \to D \in P$
11		inaghl.f	$⊢ φ \to F \in P$
12		inaghl.y	$⊢ φ \to Y \in P$
13		inaghl.1	$⊢ φ \to D K (B) A$
14		inaghl.2	$⊢ φ \to F K (B) C$
15		inaghl.3	$⊢ φ \to Y K (B) X$
16	1 2 3 10 5 6 8 13	hlne1	$⊢ φ \to D \neq B$
17	1 2 3 11 7 6 8 14	hlne1	$⊢ φ \to F \neq B$
18	1 2 3 12 4 6 8 15	hlne1	$⊢ φ \to Y \neq B$
19	16 17 18	3jca	$⊢ φ \to (D \neq B \land F \neq B \land Y \neq B)$
20	6	adantr	$⊢ (φ \land B \in (A I C)) \to B \in P$
21		eleq1	$⊢ y = B \to (y \in (D I F) \leftrightarrow B \in (D I F))$
22		eqeq1	$⊢ y = B \to (y = B \leftrightarrow B = B)$
23		breq1	$⊢ y = B \to (y K (B) Y \leftrightarrow B K (B) Y)$
24	22 23	orbi12d	$⊢ y = B \to ((y = B \lor y K (B) Y) \leftrightarrow (B = B \lor B K (B) Y))$
25	21 24	anbi12d	$⊢ y = B \to ((y \in (D I F) \land (y = B \lor y K (B) Y)) \leftrightarrow (B \in (D I F) \land (B = B \lor B K (B) Y)))$
26	25	adantl	$⊢ ((φ \land B \in (A I C)) \land y = B) \to ((y \in (D I F) \land (y = B \lor y K (B) Y)) \leftrightarrow (B \in (D I F) \land (B = B \lor B K (B) Y)))$
27	5	adantr	$⊢ (φ \land B \in (A I C)) \to A \in P$
28	10	adantr	$⊢ (φ \land B \in (A I C)) \to D \in P$
29	11	adantr	$⊢ (φ \land B \in (A I C)) \to F \in P$
30	8	adantr	$⊢ (φ \land B \in (A I C)) \to G \in 𝒢_{Tarski}$
31	1 2 3 10 5 6 8 13	hlcomd	$⊢ φ \to A K (B) D$
32	31	adantr	$⊢ (φ \land B \in (A I C)) \to A K (B) D$
33		eqid	$⊢ dist (G) = dist (G)$
34	7	adantr	$⊢ (φ \land B \in (A I C)) \to C \in P$
35	1 2 3 11 7 6 8 14	hlcomd	$⊢ φ \to C K (B) F$
36	35	adantr	$⊢ (φ \land B \in (A I C)) \to C K (B) F$
37		simpr	$⊢ (φ \land B \in (A I C)) \to B \in (A I C)$
38	1 33 2 30 27 20 34 37	tgbtwncom	$⊢ (φ \land B \in (A I C)) \to B \in (C I A)$
39	1 2 3 34 29 27 30 20 36 38	btwnhl	$⊢ (φ \land B \in (A I C)) \to B \in (F I A)$
40	1 33 2 30 29 20 27 39	tgbtwncom	$⊢ (φ \land B \in (A I C)) \to B \in (A I F)$
41	1 2 3 27 28 29 30 20 32 40	btwnhl	$⊢ (φ \land B \in (A I C)) \to B \in (D I F)$
42		eqidd	$⊢ (φ \land B \in (A I C)) \to B = B$
43	42	orcd	$⊢ (φ \land B \in (A I C)) \to (B = B \lor B K (B) Y)$
44	41 43	jca	$⊢ (φ \land B \in (A I C)) \to (B \in (D I F) \land (B = B \lor B K (B) Y))$
45	20 26 44	rspcedvd	$⊢ (φ \land B \in (A I C)) \to \exists y \in P (y \in (D I F) \land (y = B \lor y K (B) Y))$
46		simpllr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to x \in P$
47		simpr	$⊢ (((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \land y = x) \to y = x$
48	47	eleq1d	$⊢ (((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \land y = x) \to (y \in (D I F) \leftrightarrow x \in (D I F))$
49	47	eqeq1d	$⊢ (((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \land y = x) \to (y = B \leftrightarrow x = B)$
50	47	breq1d	$⊢ (((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \land y = x) \to (y K (B) Y \leftrightarrow x K (B) Y)$
51	49 50	orbi12d	$⊢ (((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \land y = x) \to ((y = B \lor y K (B) Y) \leftrightarrow (x = B \lor x K (B) Y))$
52	48 51	anbi12d	$⊢ (((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \land y = x) \to ((y \in (D I F) \land (y = B \lor y K (B) Y)) \leftrightarrow (x \in (D I F) \land (x = B \lor x K (B) Y)))$
53		simpr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to x = B$
54	5	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to A \in P$
55	10	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to D \in P$
56	11	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to F \in P$
57	8	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to G \in 𝒢_{Tarski}$
58	6	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to B \in P$
59	31	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to A K (B) D$
60	7	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to C \in P$
61	35	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to C K (B) F$
62		simplr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to x \in (A I C)$
63	1 33 2 57 54 46 60 62	tgbtwncom	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to x \in (C I A)$
64	53 63	eqeltrrd	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to B \in (C I A)$
65	1 2 3 60 56 54 57 58 61 64	btwnhl	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to B \in (F I A)$
66	1 33 2 57 56 58 54 65	tgbtwncom	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to B \in (A I F)$
67	1 2 3 54 55 56 57 58 59 66	btwnhl	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to B \in (D I F)$
68	53 67	eqeltrd	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to x \in (D I F)$
69	53	orcd	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to (x = B \lor x K (B) Y)$
70	68 69	jca	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to (x \in (D I F) \land (x = B \lor x K (B) Y))$
71	46 52 70	rspcedvd	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x = B) \to \exists y \in P (y \in (D I F) \land (y = B \lor y K (B) Y))$
72	8	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to G \in 𝒢_{Tarski}$
73	72	ad2antrr	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to G \in 𝒢_{Tarski}$
74		simplr	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to z \in P$
75	6	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to B \in P$
76	75	ad2antrr	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to B \in P$
77	7	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to C \in P$
78	77	ad2antrr	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to C \in P$
79	10	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to D \in P$
80	79	ad2antrr	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to D \in P$
81	11	ad6antr	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to F \in P$
82		simpllr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to x \in P$
83	82	ad2antrr	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to x \in P$
84		simprl	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to x K (B) z$
85	1 2 3 83 74 76 73 84	hlne2	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to z \neq B$
86	35	ad6antr	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to C K (B) F$
87		simprr	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to z \in (C I D)$
88	1 33 2 73 78 74 80 87	tgbtwncom	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to z \in (D I C)$
89	1 2 3 73 74 76 78 80 81 85 86 88	hlpasch	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to \exists y \in P (z K (B) y \land y \in (D I F))$
90		simprr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to y \in (D I F)$
91		simplr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to y \in P$
92	74	ad2antrr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to z \in P$
93	12	ad8antr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to Y \in P$
94	73	ad2antrr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to G \in 𝒢_{Tarski}$
95	76	ad2antrr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to B \in P$
96		simprl	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to z K (B) y$
97	1 2 3 92 91 95 94 96	hlcomd	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to y K (B) z$
98	82	ad4antr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to x \in P$
99	4	ad8antr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to X \in P$
100	15	ad8antr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to Y K (B) X$
101		simp-5r	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to x K (B) X$
102	1 2 3 98 99 95 94 101	hlcomd	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to X K (B) x$
103	1 2 3 93 99 98 94 95 100 102	hltr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to Y K (B) x$
104		simpllr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to (x K (B) z \land z \in (C I D))$
105	104	simpld	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to x K (B) z$
106	1 2 3 93 98 92 94 95 103 105	hltr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to Y K (B) z$
107	1 2 3 93 92 95 94 106	hlcomd	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to z K (B) Y$
108	1 2 3 91 92 93 94 95 97 107	hltr	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to y K (B) Y$
109	108	olcd	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to (y = B \lor y K (B) Y)$
110	90 109	jca	$⊢ ((((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \land (z K (B) y \land y \in (D I F))) \to (y \in (D I F) \land (y = B \lor y K (B) Y))$
111	110	ex	$⊢ (((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \land y \in P) \to ((z K (B) y \land y \in (D I F)) \to (y \in (D I F) \land (y = B \lor y K (B) Y)))$
112	111	reximdva	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to (\exists y \in P (z K (B) y \land y \in (D I F)) \to \exists y \in P (y \in (D I F) \land (y = B \lor y K (B) Y)))$
113	89 112	mpd	$⊢ ((((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \land z \in P) \land (x K (B) z \land z \in (C I D))) \to \exists y \in P (y \in (D I F) \land (y = B \lor y K (B) Y))$
114	5	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to A \in P$
115	4	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to X \in P$
116		simpr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to x K (B) X$
117	1 2 3 82 115 75 72 116	hlne1	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to x \neq B$
118	31	ad4antr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to A K (B) D$
119		simplr	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to x \in (A I C)$
120	1 33 2 72 114 82 77 119	tgbtwncom	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to x \in (C I A)$
121	1 2 3 72 82 75 114 77 79 117 118 120	hlpasch	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to \exists z \in P (x K (B) z \land z \in (C I D))$
122	113 121	r19.29a	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land x K (B) X) \to \exists y \in P (y \in (D I F) \land (y = B \lor y K (B) Y))$
123	71 122	jaodan	$⊢ ((((φ \land \neg B \in (A I C)) \land x \in P) \land x \in (A I C)) \land (x = B \lor x K (B) X)) \to \exists y \in P (y \in (D I F) \land (y = B \lor y K (B) Y))$
124	123	anasss	$⊢ (((φ \land \neg B \in (A I C)) \land x \in P) \land (x \in (A I C) \land (x = B \lor x K (B) X))) \to \exists y \in P (y \in (D I F) \land (y = B \lor y K (B) Y))$
125	1 2 3 4 5 6 7 8	isinag	$⊢ φ \to (X \in_{𝒢}^{∠} (G) ⟨“ A B C ”⟩ \leftrightarrow ((A \neq B \land C \neq B \land X \neq B) \land \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X))))$
126	9 125	mpbid	$⊢ φ \to ((A \neq B \land C \neq B \land X \neq B) \land \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X)))$
127	126	simprd	$⊢ φ \to \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X))$
128	127	adantr	$⊢ (φ \land \neg B \in (A I C)) \to \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X))$
129	124 128	r19.29a	$⊢ (φ \land \neg B \in (A I C)) \to \exists y \in P (y \in (D I F) \land (y = B \lor y K (B) Y))$
130	45 129	pm2.61dan	$⊢ φ \to \exists y \in P (y \in (D I F) \land (y = B \lor y K (B) Y))$
131	1 2 3 12 10 6 11 8	isinag	$⊢ φ \to (Y \in_{𝒢}^{∠} (G) ⟨“ D B F ”⟩ \leftrightarrow ((D \neq B \land F \neq B \land Y \neq B) \land \exists y \in P (y \in (D I F) \land (y = B \lor y K (B) Y))))$
132	19 130 131	mpbir2and	$⊢ φ \to Y \in_{𝒢}^{∠} (G) ⟨“ D B F ”⟩$

Metamath Proof Explorer

Theorem inaghl

Proof