lnopp2hpgb

	Ref	Expression
Hypotheses	ishpg.p	$⊢ P = {Base}_{G}$
	ishpg.i	$⊢ I = Itv (G)$
	ishpg.l	$⊢ L = {Line}_{𝒢} (G)$
	ishpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
	ishpg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ishpg.d	$⊢ φ \to D \in ran L$
	hpgbr.a	$⊢ φ \to A \in P$
	hpgbr.b	$⊢ φ \to B \in P$
	lnopp2hpgb.c	$⊢ φ \to C \in P$
	lnopp2hpgb.1	$⊢ φ \to A O C$
Assertion	lnopp2hpgb	$⊢ φ \to (B O C \leftrightarrow A {hp}_{𝒢} (G) (D) B)$

Proof

Step	Hyp	Ref	Expression
1		ishpg.p	$⊢ P = {Base}_{G}$
2		ishpg.i	$⊢ I = Itv (G)$
3		ishpg.l	$⊢ L = {Line}_{𝒢} (G)$
4		ishpg.o	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ D) \land b \in (P ∖ D)) \land \exists t \in D t \in (a I b))\}$
5		ishpg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		ishpg.d	$⊢ φ \to D \in ran L$
7		hpgbr.a	$⊢ φ \to A \in P$
8		hpgbr.b	$⊢ φ \to B \in P$
9		lnopp2hpgb.c	$⊢ φ \to C \in P$
10		lnopp2hpgb.1	$⊢ φ \to A O C$
11	9	adantr	$⊢ (φ \land B O C) \to C \in P$
12	10	adantr	$⊢ (φ \land B O C) \to A O C$
13		simpr	$⊢ (φ \land B O C) \to B O C$
14		breq2	$⊢ d = C \to (A O d \leftrightarrow A O C)$
15		breq2	$⊢ d = C \to (B O d \leftrightarrow B O C)$
16	14 15	anbi12d	$⊢ d = C \to ((A O d \land B O d) \leftrightarrow (A O C \land B O C))$
17	16	rspcev	$⊢ (C \in P \land (A O C \land B O C)) \to \exists d \in P (A O d \land B O d)$
18	11 12 13 17	syl12anc	$⊢ (φ \land B O C) \to \exists d \in P (A O d \land B O d)$
19	1 2 3 4 5 6 7 8	hpgbr	$⊢ φ \to (A {hp}_{𝒢} (G) (D) B \leftrightarrow \exists d \in P (A O d \land B O d))$
20	19	adantr	$⊢ (φ \land B O C) \to (A {hp}_{𝒢} (G) (D) B \leftrightarrow \exists d \in P (A O d \land B O d))$
21	18 20	mpbird	$⊢ (φ \land B O C) \to A {hp}_{𝒢} (G) (D) B$
22		eqid	$⊢ dist (G) = dist (G)$
23	6	ad7antr	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to D \in ran L$
24	23	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to D \in ran L$
25	5	ad7antr	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to G \in 𝒢_{Tarski}$
26	25	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to G \in 𝒢_{Tarski}$
27		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
28	7	ad3antrrr	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to A \in P$
29	28	ad4antr	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to A \in P$
30	29	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to A \in P$
31	8	ad3antrrr	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to B \in P$
32	31	ad4antr	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to B \in P$
33	32	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to B \in P$
34	9	ad10antr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to C \in P$
35	10	ad10antr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to A O C$
36		simpr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \in D$
37		simplr	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to y \in D$
38	1 3 2 25 23 37	tglnpt	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to y \in P$
39	38	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to y \in P$
40		simp-5r	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to y \in D$
41	1 22 2 4 3 24 26 30 34 35	oppne1	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to \neg A \in D$
42		nelne2	$⊢ (y \in D \land \neg A \in D) \to y \neq A$
43	40 41 42	syl2anc	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to y \neq A$
44	1 2 3 26 39 30 43	tgelrnln	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to y L A \in ran L$
45	1 2 3 26 39 30 43	tglinerflx2	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to A \in (y L A)$
46		nelne1	$⊢ (A \in (y L A) \land \neg A \in D) \to y L A \neq D$
47	45 41 46	syl2anc	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to y L A \neq D$
48	47	necomd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to D \neq y L A$
49		simpllr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \in P$
50		simplrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \in (y I A)$
51	1 2 3 26 39 30 49 43 50	btwnlng1	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \in (y L A)$
52	36 51	elind	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \in (D \cap (y L A))$
53	1 2 3 26 39 30 43	tglinerflx1	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to y \in (y L A)$
54	40 53	elind	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to y \in (D \cap (y L A))$
55	1 2 3 26 24 44 48 52 54	tglineineq	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z = y$
56	55 43	eqnetrd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \neq A$
57	56	necomd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to A \neq z$
58		simp-4r	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to x \in D$
59	1 3 2 25 23 58	tglnpt	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to x \in P$
60	59	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to x \in P$
61		simp-7r	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to x \in D$
62		simplr	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to d \in P$
63	62	ad4antr	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to d \in P$
64	63	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to d \in P$
65		simprr	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to B O d$
66	65	ad7antr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to B O d$
67	1 22 2 4 3 24 26 33 64 66	oppne1	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to \neg B \in D$
68		nelne2	$⊢ (x \in D \land \neg B \in D) \to x \neq B$
69	61 67 68	syl2anc	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to x \neq B$
70	1 2 3 26 60 33 69	tgelrnln	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to x L B \in ran L$
71	1 2 3 26 60 33 69	tglinerflx2	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to B \in (x L B)$
72		nelne1	$⊢ (B \in (x L B) \land \neg B \in D) \to x L B \neq D$
73	71 67 72	syl2anc	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to x L B \neq D$
74	73	necomd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to D \neq x L B$
75		simplrl	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \in (x I B)$
76	1 2 3 26 60 33 49 69 75	btwnlng1	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \in (x L B)$
77	36 76	elind	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \in (D \cap (x L B))$
78	1 2 3 26 60 33 69	tglinerflx1	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to x \in (x L B)$
79	61 78	elind	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to x \in (D \cap (x L B))$
80	1 2 3 26 24 70 74 77 79	tglineineq	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z = x$
81	80 69	eqnetrd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \neq B$
82	81	necomd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to B \neq z$
83		simprl	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to A O d$
84	83	ad7antr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to A O d$
85	1 22 2 4 3 24 26 30 64 84	oppne2	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to \neg d \in D$
86		nelne2	$⊢ (z \in D \land \neg d \in D) \to z \neq d$
87	36 85 86	syl2anc	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \neq d$
88	87	necomd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to d \neq z$
89		simpllr	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to x \in (A I d)$
90	89	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to x \in (A I d)$
91	1 22 2 26 30 60 64 90	tgbtwncom	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to x \in (d I A)$
92	80 91	eqeltrd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \in (d I A)$
93		simp-4r	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to y \in (B I d)$
94	1 22 2 26 33 39 64 93	tgbtwncom	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to y \in (d I B)$
95	55 94	eqeltrd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to z \in (d I B)$
96	1 2 26 64 49 30 33 88 92 95	tgbtwnconn2	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to (A \in (z I B) \lor B \in (z I A))$
97	1 2 27 30 33 49 26	ishlg	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to (A {hl}_{𝒢} (G) (z) B \leftrightarrow (A \neq z \land B \neq z \land (A \in (z I B) \lor B \in (z I A))))$
98	57 82 96 97	mpbir3and	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to A {hl}_{𝒢} (G) (z) B$
99	1 22 2 4 3 24 26 27 30 33 34 35 36 98	opphl	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land z \in D) \to B O C$
100	23	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to D \in ran L$
101	25	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to G \in 𝒢_{Tarski}$
102		simpllr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to z \in P$
103	32	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to B \in P$
104	9	ad10antr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to C \in P$
105	29	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to A \in P$
106	10	ad10antr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to A O C$
107		simp-5r	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to y \in D$
108	38	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to y \in P$
109		simplrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to z \in (y I A)$
110		simpr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to \neg z \in D$
111		nelne2	$⊢ (y \in D \land \neg z \in D) \to y \neq z$
112	107 110 111	syl2anc	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to y \neq z$
113	112	necomd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to z \neq y$
114	1 22 2 101 108 102 105 109 113	tgbtwnne	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to y \neq A$
115	1 2 27 108 105 102 101 105 109 114 113	btwnhl1	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to z {hl}_{𝒢} (G) (y) A$
116	1 2 27 102 105 108 101 115	hlcomd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to A {hl}_{𝒢} (G) (y) z$
117	1 22 2 4 3 100 101 27 105 102 104 106 107 116	opphl	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to z O C$
118	58	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to x \in D$
119	59	ad3antrrr	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to x \in P$
120		simplrl	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to z \in (x I B)$
121		nelne2	$⊢ (x \in D \land \neg z \in D) \to x \neq z$
122	118 110 121	syl2anc	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to x \neq z$
123	122	necomd	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to z \neq x$
124	1 22 2 101 119 102 103 120 123	tgbtwnne	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to x \neq B$
125	1 2 27 119 103 102 101 105 120 124 123	btwnhl1	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to z {hl}_{𝒢} (G) (x) B$
126	1 22 2 4 3 100 101 27 102 103 104 117 118 125	opphl	$⊢ ((((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \land \neg z \in D) \to B O C$
127	99 126	pm2.61dan	$⊢ (((((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \land z \in P) \land (z \in (x I B) \land z \in (y I A))) \to B O C$
128		simpr	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to y \in (B I d)$
129	1 22 2 25 29 32 63 59 38 89 128	axtgpasch	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to \exists z \in P (z \in (x I B) \land z \in (y I A))$
130	127 129	r19.29a	$⊢ (((((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \land y \in D) \land y \in (B I d)) \to B O C$
131	1 22 2 4 31 62	islnopp	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to (B O d \leftrightarrow ((\neg B \in D \land \neg d \in D) \land \exists t \in D t \in (B I d)))$
132	65 131	mpbid	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to ((\neg B \in D \land \neg d \in D) \land \exists t \in D t \in (B I d))$
133	132	simprd	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to \exists t \in D t \in (B I d)$
134		eleq1w	$⊢ t = y \to (t \in (B I d) \leftrightarrow y \in (B I d))$
135	134	cbvrexvw	$⊢ \exists t \in D t \in (B I d) \leftrightarrow \exists y \in D y \in (B I d)$
136	133 135	sylib	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to \exists y \in D y \in (B I d)$
137	136	ad2antrr	$⊢ (((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \to \exists y \in D y \in (B I d)$
138	130 137	r19.29a	$⊢ (((((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \land x \in D) \land x \in (A I d)) \to B O C$
139	1 22 2 4 28 62	islnopp	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to (A O d \leftrightarrow ((\neg A \in D \land \neg d \in D) \land \exists t \in D t \in (A I d)))$
140	83 139	mpbid	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to ((\neg A \in D \land \neg d \in D) \land \exists t \in D t \in (A I d))$
141	140	simprd	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to \exists t \in D t \in (A I d)$
142		eleq1w	$⊢ t = x \to (t \in (A I d) \leftrightarrow x \in (A I d))$
143	142	cbvrexvw	$⊢ \exists t \in D t \in (A I d) \leftrightarrow \exists x \in D x \in (A I d)$
144	141 143	sylib	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to \exists x \in D x \in (A I d)$
145	138 144	r19.29a	$⊢ (((φ \land A {hp}_{𝒢} (G) (D) B) \land d \in P) \land (A O d \land B O d)) \to B O C$
146	19	biimpa	$⊢ (φ \land A {hp}_{𝒢} (G) (D) B) \to \exists d \in P (A O d \land B O d)$
147	145 146	r19.29a	$⊢ (φ \land A {hp}_{𝒢} (G) (D) B) \to B O C$
148	21 147	impbida	$⊢ φ \to (B O C \leftrightarrow A {hp}_{𝒢} (G) (D) B)$

Metamath Proof Explorer

Theorem lnopp2hpgb

Proof