plngrotlem1

	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}$
	plngrot.x	$⊢ φ \to X \in (P ∖ (Z L Y))$
	plngrot.y	$⊢ φ \to Y \in P$
	plngrot.z	$⊢ φ \to Z \in (P ∖ (X L Y))$
	plngrot.1	$⊢ φ \to X \neq Y$
	plngrotlem2.4	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Y)) \land b \in (P ∖ (X L Y))) \land \exists t \in (X L Y) t \in (a I b))\}$
	plngrotlem2.1	$⊢ φ \to W \in P$
	plngrotlem2.2	$⊢ φ \to Y \in (Z I W)$
	plngrotlem2.3	$⊢ φ \to Y \neq W$
	plngrotlem1.1	$⊢ φ \to S \in ((X L Y) E Z)$
	plngrotlem1.2	$⊢ φ \to (S \in (X L Y) \lor S {hp}_{𝒢} (G) (X L Y) Z)$
Assertion	plngrotlem1	$⊢ φ \to S \in ((Z L Y) E X)$

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		plngrot.x	$⊢ φ \to X \in (P ∖ (Z L Y))$
7		plngrot.y	$⊢ φ \to Y \in P$
8		plngrot.z	$⊢ φ \to Z \in (P ∖ (X L Y))$
9		plngrot.1	$⊢ φ \to X \neq Y$
10		plngrotlem2.4	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Y)) \land b \in (P ∖ (X L Y))) \land \exists t \in (X L Y) t \in (a I b))\}$
11		plngrotlem2.1	$⊢ φ \to W \in P$
12		plngrotlem2.2	$⊢ φ \to Y \in (Z I W)$
13		plngrotlem2.3	$⊢ φ \to Y \neq W$
14		plngrotlem1.1	$⊢ φ \to S \in ((X L Y) E Z)$
15		plngrotlem1.2	$⊢ φ \to (S \in (X L Y) \lor S {hp}_{𝒢} (G) (X L Y) Z)$
16	8	eldifad	$⊢ φ \to Z \in P$
17	6	eldifad	$⊢ φ \to X \in P$
18	1 2 3 5 17 7 9	tglinerflx2	$⊢ φ \to Y \in (X L Y)$
19		elndif	$⊢ Y \in (X L Y) \to \neg Y \in (P ∖ (X L Y))$
20	18 19	syl	$⊢ φ \to \neg Y \in (P ∖ (X L Y))$
21		nelne2	$⊢ (Z \in (P ∖ (X L Y)) \land \neg Y \in (P ∖ (X L Y))) \to Z \neq Y$
22	8 20 21	syl2anc	$⊢ φ \to Z \neq Y$
23	1 2 3 5 16 7 22	tgelrnln	$⊢ φ \to Z L Y \in ran L$
24	1 2 3 4 5 23 6	elplnglnid	$⊢ φ \to Z L Y \subseteq (Z L Y) E X$
25	24	sselda	$⊢ (φ \land S \in (Z L Y)) \to S \in ((Z L Y) E X)$
26	5	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to G \in 𝒢_{Tarski}$
27	26	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to G \in 𝒢_{Tarski}$
28	23	ad3antrrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to Z L Y \in ran L$
29	1 2 3 5 17 7 9	tgelrnln	$⊢ φ \to X L Y \in ran L$
30	1 2 3 4 5 29 8 14	plngssp	$⊢ φ \to S \in P$
31	30	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to S \in P$
32	11	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to W \in P$
33		simpr	$⊢ (φ \land S = W) \to S = W$
34	1 2 3 5 16 7 11 22 12	btwnlng3	$⊢ φ \to W \in (Z L Y)$
35	34	adantr	$⊢ (φ \land S = W) \to W \in (Z L Y)$
36	33 35	eqeltrd	$⊢ (φ \land S = W) \to S \in (Z L Y)$
37	36	stoic1a	$⊢ (φ \land \neg S \in (Z L Y)) \to \neg S = W$
38	37	neqned	$⊢ (φ \land \neg S \in (Z L Y)) \to S \neq W$
39	1 2 3 26 31 32 38	tgelrnln	$⊢ (φ \land \neg S \in (Z L Y)) \to S L W \in ran L$
40	39	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to S L W \in ran L$
41	31	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to S \in P$
42	32	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to W \in P$
43	29	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to X L Y \in ran L$
44	43	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to X L Y \in ran L$
45		simplr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to t \in (X L Y)$
46	1 3 2 27 44 45	tglnpt	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to t \in P$
47	38	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to S \neq W$
48		eqid	$⊢ dist (G) = dist (G)$
49		simpr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to t \in (W I S)$
50	1 48 2 27 42 46 41 49	tgbtwncom	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to t \in (S I W)$
51	1 2 3 27 41 42 46 47 50	btwnlng1	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to t \in (S L W)$
52	13	neneqd	$⊢ φ \to \neg Y = W$
53	52	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to \neg Y = W$
54	5	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to G \in 𝒢_{Tarski}$
55	29	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to X L Y \in ran L$
56	23	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to Z L Y \in ran L$
57	16	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to Z \in P$
58	7	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to Y \in P$
59	22	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to Z \neq Y$
60	1 2 3 26 57 58 59	tglinerflx1	$⊢ (φ \land \neg S \in (Z L Y)) \to Z \in (Z L Y)$
61	8	eldifbd	$⊢ φ \to \neg Z \in (X L Y)$
62	61	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to \neg Z \in (X L Y)$
63		nelne1	$⊢ (Z \in (Z L Y) \land \neg Z \in (X L Y)) \to Z L Y \neq X L Y$
64	60 62 63	syl2an2r	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to Z L Y \neq X L Y$
65	64	necomd	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to X L Y \neq Z L Y$
66	18	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to Y \in (X L Y)$
67	16	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to Z \in P$
68	7	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to Y \in P$
69	22	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to Z \neq Y$
70	1 2 3 54 67 68 69	tglinerflx2	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to Y \in (Z L Y)$
71	66 70	elind	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to Y \in ((X L Y) \cap (Z L Y))$
72		simpr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to W \in (X L Y)$
73	11	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to W \in P$
74	12	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to Y \in (Z I W)$
75	1 2 3 54 67 68 73 69 74	btwnlng3	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to W \in (Z L Y)$
76	72 75	elind	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to W \in ((X L Y) \cap (Z L Y))$
77	1 2 3 54 55 56 65 71 76	tglineineq	$⊢ ((φ \land \neg S \in (Z L Y)) \land W \in (X L Y)) \to Y = W$
78	53 77	mtand	$⊢ (φ \land \neg S \in (Z L Y)) \to \neg W \in (X L Y)$
79	78	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to \neg W \in (X L Y)$
80		nelne2	$⊢ (t \in (X L Y) \land \neg W \in (X L Y)) \to t \neq W$
81	45 79 80	syl2anc	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to t \neq W$
82	1 2 3 27 41 42 47	tglinerflx1	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to S \in (S L W)$
83		simpllr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to \neg S \in (Z L Y)$
84		nelne1	$⊢ (S \in (S L W) \land \neg S \in (Z L Y)) \to S L W \neq Z L Y$
85	82 83 84	syl2anc	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to S L W \neq Z L Y$
86	85	necomd	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to Z L Y \neq S L W$
87	34	ad3antrrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to W \in (Z L Y)$
88	1 2 3 27 41 42 47	tglinerflx2	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to W \in (S L W)$
89	87 88	elind	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to W \in ((Z L Y) \cap (S L W))$
90	1 2 3 27 28 40 86 89	tglineinsn	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to (Z L Y) \cap (S L W) = \{W\}$
91	1 2 3 4 27 28 40 51 42 81 90	lnincplng	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to S L W \subseteq (Z L Y) E t$
92	6	ad3antrrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to X \in (P ∖ (Z L Y))$
93	17	ad3antrrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to X \in P$
94	58	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to Y \in P$
95	9	ad3antrrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to X \neq Y$
96	1 2 3 27 93 94 95	tglinerflx1	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to X \in (X L Y)$
97	60	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to Z \in (Z L Y)$
98	61	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to \neg Z \in (X L Y)$
99	98	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to \neg Z \in (X L Y)$
100	97 99 63	syl2anc	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to Z L Y \neq X L Y$
101	57	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to Z \in P$
102	59	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to Z \neq Y$
103	1 2 3 27 101 94 102	tglinerflx2	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to Y \in (Z L Y)$
104	18	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to Y \in (X L Y)$
105	104	ad2antrr	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to Y \in (X L Y)$
106	103 105	elind	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to Y \in ((Z L Y) \cap (X L Y))$
107	1 2 3 27 28 44 100 106	tglineinsn	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to (Z L Y) \cap (X L Y) = \{Y\}$
108	1 2 3 4 27 28 44 96 94 95 107	lnincplng	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to X L Y \subseteq (Z L Y) E X$
109	108 45	sseldd	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to t \in ((Z L Y) E X)$
110	27	adantr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to G \in 𝒢_{Tarski}$
111	46	adantr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to t \in P$
112	42	adantr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to W \in P$
113	41	adantr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to S \in P$
114	81	adantr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to t \neq W$
115	50	adantr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to t \in (S I W)$
116	1 2 3 110 111 112 113 114 115	btwnlng2	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to S \in (t L W)$
117	57	ad3antrrr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to Z \in P$
118	99	adantr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to \neg Z \in (X L Y)$
119		nelne2	$⊢ (t \in (X L Y) \land \neg Z \in (X L Y)) \to t \neq Z$
120	45 118 119	syl2an2r	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to t \neq Z$
121	120	necomd	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to Z \neq t$
122	1 2 3 110 117 111 121	tglinecom	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to Z L t = t L Z$
123	22	necomd	$⊢ φ \to Y \neq Z$
124	1 48 2 5 16 7 11 12 123	tgbtwnne	$⊢ φ \to Z \neq W$
125	124	ad4antr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to Z \neq W$
126		simpr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to t \in (Z L Y)$
127	1 2 3 5 16 11 7 124 12	btwnlng1	$⊢ φ \to Y \in (Z L W)$
128	1 2 3 5 16 11 124 7 123 127	tglineelsb2	$⊢ φ \to Z L W = Z L Y$
129	128	ad4antr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to Z L W = Z L Y$
130	126 129	eleqtrrd	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to t \in (Z L W)$
131	1 2 3 110 117 112 125 111 120 130	tglineelsb2	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to Z L W = Z L t$
132	131 129	eqtr3d	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to Z L t = Z L Y$
133	81	necomd	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to W \neq t$
134	133	adantr	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to W \neq t$
135	1 2 3 110 111 117 112 120 130 125	lnrot2	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to W \in (t L Z)$
136	1 2 3 110 111 117 120 112 134 135	tglineelsb2	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to t L Z = t L W$
137	122 132 136	3eqtr3rd	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to t L W = Z L Y$
138	116 137	eleqtrd	$⊢ ((((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \land t \in (Z L Y)) \to S \in (Z L Y)$
139	83 138	mtand	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to \neg t \in (Z L Y)$
140	109 139	eldifd	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to t \in (((Z L Y) E X) ∖ (Z L Y))$
141	1 2 3 4 27 28 92 140	plngcp	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to (Z L Y) E X = (Z L Y) E t$
142	91 141	sseqtrrd	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to S L W \subseteq (Z L Y) E X$
143	142 82	sseldd	$⊢ (((φ \land \neg S \in (Z L Y)) \land t \in (X L Y)) \land t \in (W I S)) \to S \in ((Z L Y) E X)$
144		eleq1	$⊢ t = S \to (t \in (W I S) \leftrightarrow S \in (W I S))$
145		simpr	$⊢ ((φ \land \neg S \in (Z L Y)) \land S \in (X L Y)) \to S \in (X L Y)$
146	5	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land S \in (X L Y)) \to G \in 𝒢_{Tarski}$
147	11	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land S \in (X L Y)) \to W \in P$
148	30	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land S \in (X L Y)) \to S \in P$
149	1 48 2 146 147 148	tgbtwntriv2	$⊢ ((φ \land \neg S \in (Z L Y)) \land S \in (X L Y)) \to S \in (W I S)$
150	144 145 149	rspcedvdw	$⊢ ((φ \land \neg S \in (Z L Y)) \land S \in (X L Y)) \to \exists t \in (X L Y) t \in (W I S)$
151	29	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to X L Y \in ran L$
152	5	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to G \in 𝒢_{Tarski}$
153	30	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to S \in P$
154	11	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to W \in P$
155	16	ad2antrr	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to Z \in P$
156	15	ord	$⊢ φ \to (\neg S \in (X L Y) \to S {hp}_{𝒢} (G) (X L Y) Z)$
157	156	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to (\neg S \in (X L Y) \to S {hp}_{𝒢} (G) (X L Y) Z)$
158	157	imp	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to S {hp}_{𝒢} (G) (X L Y) Z$
159	1 2 3 152 151 153 10 155 158	hpgcom	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to Z {hp}_{𝒢} (G) (X L Y) S$
160	12	adantr	$⊢ (φ \land \neg S \in (Z L Y)) \to Y \in (Z I W)$
161	1 48 2 10 57 32 104 98 78 160	islnoppd	$⊢ (φ \land \neg S \in (Z L Y)) \to Z O W$
162	1 2 3 10 26 43 57 31 32 161	lnopp2hpgb	$⊢ (φ \land \neg S \in (Z L Y)) \to (S O W \leftrightarrow Z {hp}_{𝒢} (G) (X L Y) S)$
163	162	adantr	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to (S O W \leftrightarrow Z {hp}_{𝒢} (G) (X L Y) S)$
164	159 163	mpbird	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to S O W$
165	1 48 2 10 3 151 152 153 154 164	oppcom	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to W O S$
166	1 48 2 10 154 153	islnopp	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to (W O S \leftrightarrow ((\neg W \in (X L Y) \land \neg S \in (X L Y)) \land \exists t \in (X L Y) t \in (W I S)))$
167	165 166	mpbid	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to ((\neg W \in (X L Y) \land \neg S \in (X L Y)) \land \exists t \in (X L Y) t \in (W I S))$
168	167	simprd	$⊢ ((φ \land \neg S \in (Z L Y)) \land \neg S \in (X L Y)) \to \exists t \in (X L Y) t \in (W I S)$
169		exmidd	$⊢ (φ \land \neg S \in (Z L Y)) \to (S \in (X L Y) \lor \neg S \in (X L Y))$
170	150 168 169	mpjaodan	$⊢ (φ \land \neg S \in (Z L Y)) \to \exists t \in (X L Y) t \in (W I S)$
171	143 170	r19.29a	$⊢ (φ \land \neg S \in (Z L Y)) \to S \in ((Z L Y) E X)$
172		exmidd	$⊢ φ \to (S \in (Z L Y) \lor \neg S \in (Z L Y))$
173	25 171 172	mpjaodan	$⊢ φ \to S \in ((Z L Y) E X)$

Metamath Proof Explorer

Theorem plngrotlem1

Proof