plngcplem

	Ref	Expression
Hypotheses	plngval.p	$⊢ P = {Base}_{G}$
	plngval.i	$⊢ I = Itv (G)$
	plngval.1	$⊢ L = {Line}_{𝒢} (G)$
	plngval.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	plngcp.a	$⊢ φ \to A \in ran L$
	plngcp.r	$⊢ φ \to R \in (P ∖ A)$
	plngcp.s	$⊢ φ \to S \in ((A E R) ∖ A)$
	plngcplem.1	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\}$
Assertion	plngcplem	$⊢ φ \to A E R = A E S$

Proof

Step	Hyp	Ref	Expression
1		plngval.p	$⊢ P = {Base}_{G}$
2		plngval.i	$⊢ I = Itv (G)$
3		plngval.1	$⊢ L = {Line}_{𝒢} (G)$
4		plngval.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
5		plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		plngcp.a	$⊢ φ \to A \in ran L$
7		plngcp.r	$⊢ φ \to R \in (P ∖ A)$
8		plngcp.s	$⊢ φ \to S \in ((A E R) ∖ A)$
9		plngcplem.1	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ A) \land b \in (P ∖ A)) \land \exists t \in A t \in (a I b))\}$
10	5	ad2antrr	$⊢ ((φ \land x \in P) \land S O R) \to G \in 𝒢_{Tarski}$
11	6	ad2antrr	$⊢ ((φ \land x \in P) \land S O R) \to A \in ran L$
12	7	eldifad	$⊢ φ \to R \in P$
13	12	ad2antrr	$⊢ ((φ \land x \in P) \land S O R) \to R \in P$
14		simplr	$⊢ ((φ \land x \in P) \land S O R) \to x \in P$
15	8	eldifad	$⊢ φ \to S \in (A E R)$
16	1 2 3 4 5 6 7 15	plngssp	$⊢ φ \to S \in P$
17	16	ad2antrr	$⊢ ((φ \land x \in P) \land S O R) \to S \in P$
18		eqid	$⊢ dist (G) = dist (G)$
19		simpr	$⊢ ((φ \land x \in P) \land S O R) \to S O R$
20	1 18 2 9 3 11 10 17 13 19	oppcom	$⊢ ((φ \land x \in P) \land S O R) \to R O S$
21	1 2 3 9 10 11 13 14 17 20	lnopp2hpgb	$⊢ ((φ \land x \in P) \land S O R) \to (x O S \leftrightarrow R {hp}_{𝒢} (G) (A) x)$
22	21	adantlr	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S O R) \to (x O S \leftrightarrow R {hp}_{𝒢} (G) (A) x)$
23	5	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land R {hp}_{𝒢} (G) (A) x) \to G \in 𝒢_{Tarski}$
24	6	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land R {hp}_{𝒢} (G) (A) x) \to A \in ran L$
25	12	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land R {hp}_{𝒢} (G) (A) x) \to R \in P$
26		simp-4r	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land R {hp}_{𝒢} (G) (A) x) \to x \in P$
27		simpr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land R {hp}_{𝒢} (G) (A) x) \to R {hp}_{𝒢} (G) (A) x$
28	1 2 3 23 24 25 9 26 27	hpgcom	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land R {hp}_{𝒢} (G) (A) x) \to x {hp}_{𝒢} (G) (A) R$
29	5	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) R) \to G \in 𝒢_{Tarski}$
30	6	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) R) \to A \in ran L$
31		simp-4r	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) R) \to x \in P$
32	12	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) R) \to R \in P$
33		simpr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) R) \to x {hp}_{𝒢} (G) (A) R$
34	1 2 3 29 30 31 9 32 33	hpgcom	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) R) \to R {hp}_{𝒢} (G) (A) x$
35	28 34	impbida	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S O R) \to (R {hp}_{𝒢} (G) (A) x \leftrightarrow x {hp}_{𝒢} (G) (A) R)$
36	22 35	bitr2d	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S O R) \to (x {hp}_{𝒢} (G) (A) R \leftrightarrow x O S)$
37	1 2 3 9 10 11 17 14 13 19	lnopp2hpgb	$⊢ ((φ \land x \in P) \land S O R) \to (x O R \leftrightarrow S {hp}_{𝒢} (G) (A) x)$
38	37	adantlr	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S O R) \to (x O R \leftrightarrow S {hp}_{𝒢} (G) (A) x)$
39	5	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land S {hp}_{𝒢} (G) (A) x) \to G \in 𝒢_{Tarski}$
40	6	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land S {hp}_{𝒢} (G) (A) x) \to A \in ran L$
41	16	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land S {hp}_{𝒢} (G) (A) x) \to S \in P$
42		simp-4r	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land S {hp}_{𝒢} (G) (A) x) \to x \in P$
43		simpr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land S {hp}_{𝒢} (G) (A) x) \to S {hp}_{𝒢} (G) (A) x$
44	1 2 3 39 40 41 9 42 43	hpgcom	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land S {hp}_{𝒢} (G) (A) x) \to x {hp}_{𝒢} (G) (A) S$
45	5	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) S) \to G \in 𝒢_{Tarski}$
46	6	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) S) \to A \in ran L$
47		simp-4r	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) S) \to x \in P$
48	16	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) S) \to S \in P$
49		simpr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) S) \to x {hp}_{𝒢} (G) (A) S$
50	1 2 3 45 46 47 9 48 49	hpgcom	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S O R) \land x {hp}_{𝒢} (G) (A) S) \to S {hp}_{𝒢} (G) (A) x$
51	44 50	impbida	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S O R) \to (S {hp}_{𝒢} (G) (A) x \leftrightarrow x {hp}_{𝒢} (G) (A) S)$
52	38 51	bitrd	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S O R) \to (x O R \leftrightarrow x {hp}_{𝒢} (G) (A) S)$
53	36 52	orbi12d	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S O R) \to ((x {hp}_{𝒢} (G) (A) R \lor x O R) \leftrightarrow (x O S \lor x {hp}_{𝒢} (G) (A) S))$
54		orcom	$⊢ (x O S \lor x {hp}_{𝒢} (G) (A) S) \leftrightarrow (x {hp}_{𝒢} (G) (A) S \lor x O S)$
55	53 54	bitrdi	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S O R) \to ((x {hp}_{𝒢} (G) (A) R \lor x O R) \leftrightarrow (x {hp}_{𝒢} (G) (A) S \lor x O S))$
56	5	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) R) \to G \in 𝒢_{Tarski}$
57	6	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) R) \to A \in ran L$
58		simp-4r	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) R) \to x \in P$
59	12	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) R) \to R \in P$
60		simpr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) R) \to x {hp}_{𝒢} (G) (A) R$
61	16	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) R) \to S \in P$
62		simplr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) R) \to S {hp}_{𝒢} (G) (A) R$
63	1 2 3 56 57 61 9 59 62	hpgcom	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) R) \to R {hp}_{𝒢} (G) (A) S$
64	1 2 3 56 57 58 9 59 60 61 63	hpgtr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) R) \to x {hp}_{𝒢} (G) (A) S$
65	5	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) S) \to G \in 𝒢_{Tarski}$
66	6	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) S) \to A \in ran L$
67		simp-4r	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) S) \to x \in P$
68	16	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) S) \to S \in P$
69		simpr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) S) \to x {hp}_{𝒢} (G) (A) S$
70	12	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) S) \to R \in P$
71		simplr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) S) \to S {hp}_{𝒢} (G) (A) R$
72	1 2 3 65 66 67 9 68 69 70 71	hpgtr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x {hp}_{𝒢} (G) (A) S) \to x {hp}_{𝒢} (G) (A) R$
73	64 72	impbida	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \to (x {hp}_{𝒢} (G) (A) R \leftrightarrow x {hp}_{𝒢} (G) (A) S)$
74	6	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to A \in ran L$
75	5	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to G \in 𝒢_{Tarski}$
76	16	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to S \in P$
77		simp-4r	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to x \in P$
78	12	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to R \in P$
79		simplr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to S {hp}_{𝒢} (G) (A) R$
80	1 2 3 75 74 76 9 78 79	hpgcom	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to R {hp}_{𝒢} (G) (A) S$
81		simpr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to x O R$
82	1 18 2 9 3 74 75 77 78 81	oppcom	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to R O x$
83	1 2 3 9 75 74 78 76 77 82	lnopp2hpgb	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to (S O x \leftrightarrow R {hp}_{𝒢} (G) (A) S)$
84	80 83	mpbird	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to S O x$
85	1 18 2 9 3 74 75 76 77 84	oppcom	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O R) \to x O S$
86	6	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to A \in ran L$
87	5	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to G \in 𝒢_{Tarski}$
88	12	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to R \in P$
89		simp-4r	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to x \in P$
90		simplr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to S {hp}_{𝒢} (G) (A) R$
91	16	ad4antr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to S \in P$
92		simpr	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to x O S$
93	1 18 2 9 3 86 87 89 91 92	oppcom	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to S O x$
94	1 2 3 9 87 86 91 88 89 93	lnopp2hpgb	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to (R O x \leftrightarrow S {hp}_{𝒢} (G) (A) R)$
95	90 94	mpbird	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to R O x$
96	1 18 2 9 3 86 87 88 89 95	oppcom	$⊢ ((((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \land x O S) \to x O R$
97	85 96	impbida	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \to (x O R \leftrightarrow x O S)$
98	73 97	orbi12d	$⊢ (((φ \land x \in P) \land \neg x \in A) \land S {hp}_{𝒢} (G) (A) R) \to ((x {hp}_{𝒢} (G) (A) R \lor x O R) \leftrightarrow (x {hp}_{𝒢} (G) (A) S \lor x O S))$
99		eleq1	$⊢ y = S \to (y \in A \leftrightarrow S \in A)$
100		breq1	$⊢ y = S \to (y {hp}_{𝒢} (G) (A) R \leftrightarrow S {hp}_{𝒢} (G) (A) R)$
101		oveq1	$⊢ y = S \to y I R = S I R$
102	101	eleq2d	$⊢ y = S \to (t \in (y I R) \leftrightarrow t \in (S I R))$
103	102	rexbidv	$⊢ y = S \to (\exists t \in A t \in (y I R) \leftrightarrow \exists t \in A t \in (S I R))$
104	99 100 103	3orbi123d	$⊢ y = S \to ((y \in A \lor y {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (y I R)) \leftrightarrow (S \in A \lor S {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (S I R)))$
105	1 2 3 4 5 6 7	plngval	$⊢ φ \to A E R = \{y \in P \| (y \in A \lor y {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (y I R))\}$
106	15 105	eleqtrd	$⊢ φ \to S \in \{y \in P \| (y \in A \lor y {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (y I R))\}$
107	104 106	elrabrd	$⊢ φ \to (S \in A \lor S {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (S I R))$
108		3orass	$⊢ (S \in A \lor S {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (S I R)) \leftrightarrow (S \in A \lor (S {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (S I R)))$
109	107 108	sylib	$⊢ φ \to (S \in A \lor (S {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (S I R)))$
110	8	eldifbd	$⊢ φ \to \neg S \in A$
111	109 110	orcnd	$⊢ φ \to (S {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (S I R))$
112	1 18 2 9 16 12	islnopp	$⊢ φ \to (S O R \leftrightarrow ((\neg S \in A \land \neg R \in A) \land \exists t \in A t \in (S I R)))$
113	7	eldifbd	$⊢ φ \to \neg R \in A$
114	110 113	jca	$⊢ φ \to (\neg S \in A \land \neg R \in A)$
115	114	biantrurd	$⊢ φ \to (\exists t \in A t \in (S I R) \leftrightarrow ((\neg S \in A \land \neg R \in A) \land \exists t \in A t \in (S I R)))$
116	112 115	bitr4d	$⊢ φ \to (S O R \leftrightarrow \exists t \in A t \in (S I R))$
117	116	orbi2d	$⊢ φ \to ((S {hp}_{𝒢} (G) (A) R \lor S O R) \leftrightarrow (S {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (S I R)))$
118	111 117	mpbird	$⊢ φ \to (S {hp}_{𝒢} (G) (A) R \lor S O R)$
119	118	orcomd	$⊢ φ \to (S O R \lor S {hp}_{𝒢} (G) (A) R)$
120	119	ad2antrr	$⊢ ((φ \land x \in P) \land \neg x \in A) \to (S O R \lor S {hp}_{𝒢} (G) (A) R)$
121	55 98 120	mpjaodan	$⊢ ((φ \land x \in P) \land \neg x \in A) \to ((x {hp}_{𝒢} (G) (A) R \lor x O R) \leftrightarrow (x {hp}_{𝒢} (G) (A) S \lor x O S))$
122		simpr	$⊢ ((φ \land x \in P) \land \neg x \in A) \to \neg x \in A$
123	113	ad2antrr	$⊢ ((φ \land x \in P) \land \neg x \in A) \to \neg R \in A$
124	122 123	jca	$⊢ ((φ \land x \in P) \land \neg x \in A) \to (\neg x \in A \land \neg R \in A)$
125	124	biantrurd	$⊢ ((φ \land x \in P) \land \neg x \in A) \to (\exists t \in A t \in (x I R) \leftrightarrow ((\neg x \in A \land \neg R \in A) \land \exists t \in A t \in (x I R)))$
126		simpr	$⊢ (φ \land x \in P) \to x \in P$
127	12	adantr	$⊢ (φ \land x \in P) \to R \in P$
128	1 18 2 9 126 127	islnopp	$⊢ (φ \land x \in P) \to (x O R \leftrightarrow ((\neg x \in A \land \neg R \in A) \land \exists t \in A t \in (x I R)))$
129	128	adantr	$⊢ ((φ \land x \in P) \land \neg x \in A) \to (x O R \leftrightarrow ((\neg x \in A \land \neg R \in A) \land \exists t \in A t \in (x I R)))$
130	125 129	bitr4d	$⊢ ((φ \land x \in P) \land \neg x \in A) \to (\exists t \in A t \in (x I R) \leftrightarrow x O R)$
131	130	orbi2d	$⊢ ((φ \land x \in P) \land \neg x \in A) \to ((x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R)) \leftrightarrow (x {hp}_{𝒢} (G) (A) R \lor x O R))$
132	110	ad2antrr	$⊢ ((φ \land x \in P) \land \neg x \in A) \to \neg S \in A$
133	122 132	jca	$⊢ ((φ \land x \in P) \land \neg x \in A) \to (\neg x \in A \land \neg S \in A)$
134	133	biantrurd	$⊢ ((φ \land x \in P) \land \neg x \in A) \to (\exists t \in A t \in (x I S) \leftrightarrow ((\neg x \in A \land \neg S \in A) \land \exists t \in A t \in (x I S)))$
135	16	adantr	$⊢ (φ \land x \in P) \to S \in P$
136	1 18 2 9 126 135	islnopp	$⊢ (φ \land x \in P) \to (x O S \leftrightarrow ((\neg x \in A \land \neg S \in A) \land \exists t \in A t \in (x I S)))$
137	136	adantr	$⊢ ((φ \land x \in P) \land \neg x \in A) \to (x O S \leftrightarrow ((\neg x \in A \land \neg S \in A) \land \exists t \in A t \in (x I S)))$
138	134 137	bitr4d	$⊢ ((φ \land x \in P) \land \neg x \in A) \to (\exists t \in A t \in (x I S) \leftrightarrow x O S)$
139	138	orbi2d	$⊢ ((φ \land x \in P) \land \neg x \in A) \to ((x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S)) \leftrightarrow (x {hp}_{𝒢} (G) (A) S \lor x O S))$
140	121 131 139	3bitr4d	$⊢ ((φ \land x \in P) \land \neg x \in A) \to ((x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R)) \leftrightarrow (x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S)))$
141	140	pm5.74da	$⊢ (φ \land x \in P) \to ((\neg x \in A \to (x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))) \leftrightarrow (\neg x \in A \to (x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S))))$
142		3orass	$⊢ (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R)) \leftrightarrow (x \in A \lor (x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R)))$
143		df-or	$⊢ (x \in A \lor (x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))) \leftrightarrow (\neg x \in A \to (x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R)))$
144	142 143	bitri	$⊢ (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R)) \leftrightarrow (\neg x \in A \to (x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R)))$
145		3orass	$⊢ (x \in A \lor x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S)) \leftrightarrow (x \in A \lor (x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S)))$
146		df-or	$⊢ (x \in A \lor (x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S))) \leftrightarrow (\neg x \in A \to (x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S)))$
147	145 146	bitri	$⊢ (x \in A \lor x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S)) \leftrightarrow (\neg x \in A \to (x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S)))$
148	141 144 147	3bitr4g	$⊢ (φ \land x \in P) \to ((x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R)) \leftrightarrow (x \in A \lor x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S)))$
149	148	rabbidva	$⊢ φ \to \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\} = \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S))\}$
150	1 2 3 4 5 6 7	plngval	$⊢ φ \to A E R = \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) R \lor \exists t \in A t \in (x I R))\}$
151	16 110	eldifd	$⊢ φ \to S \in (P ∖ A)$
152	1 2 3 4 5 6 151	plngval	$⊢ φ \to A E S = \{x \in P \| (x \in A \lor x {hp}_{𝒢} (G) (A) S \lor \exists t \in A t \in (x I S))\}$
153	149 150 152	3eqtr4d	$⊢ φ \to A E R = A E S$

Metamath Proof Explorer

Theorem plngcplem

Proof