plngrotlem2

	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$
Assertion	plngrotlem2	$⊢ φ \to (X L Y) E Z \subseteq (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	5	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to G \in 𝒢_{Tarski}$
15	6	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to X \in (P ∖ (Z L Y))$
16	7	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to Y \in P$
17	8	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to Z \in (P ∖ (X L Y))$
18	9	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to X \neq Y$
19	11	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to W \in P$
20	12	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to Y \in (Z I W)$
21	13	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to Y \neq W$
22		simpr	$⊢ (φ \land s \in ((X L Y) E Z)) \to s \in ((X L Y) E Z)$
23	22	adantr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to s \in ((X L Y) E Z)$
24		simpr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)$
25	1 2 3 4 14 15 16 17 18 10 19 20 21 23 24	plngrotlem1	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z)) \to s \in ((Z L Y) E X)$
26	5	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to G \in 𝒢_{Tarski}$
27	6	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to X \in (P ∖ (Z L Y))$
28	8	eldifad	$⊢ φ \to Z \in P$
29	28	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Z \in P$
30	7	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Y \in P$
31	6	eldifad	$⊢ φ \to X \in P$
32	1 2 3 5 31 7 9	tglinerflx2	$⊢ φ \to Y \in (X L Y)$
33		elndif	$⊢ Y \in (X L Y) \to \neg Y \in (P ∖ (X L Y))$
34	32 33	syl	$⊢ φ \to \neg Y \in (P ∖ (X L Y))$
35		nelne2	$⊢ (Z \in (P ∖ (X L Y)) \land \neg Y \in (P ∖ (X L Y))) \to Z \neq Y$
36	8 34 35	syl2anc	$⊢ φ \to Z \neq Y$
37	36	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Z \neq Y$
38	1 2 3 26 29 30 37	tglinecom	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Z L Y = Y L Z$
39	11	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to W \in P$
40	13	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Y \neq W$
41	1 2 3 5 7 11 28 13 12	btwnlng2	$⊢ φ \to Z \in (Y L W)$
42	41	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Z \in (Y L W)$
43	1 2 3 26 30 39 40 29 37 42	tglineelsb2	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Y L W = Y L Z$
44	1 2 3 26 30 39 40	tglinecom	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Y L W = W L Y$
45	38 43 44	3eqtr2d	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Z L Y = W L Y$
46	45	difeq2d	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to P ∖ (Z L Y) = P ∖ (W L Y)$
47	27 46	eleqtrd	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to X \in (P ∖ (W L Y))$
48	13	neneqd	$⊢ φ \to \neg Y = W$
49	5	adantr	$⊢ (φ \land W \in (X L Y)) \to G \in 𝒢_{Tarski}$
50	31	adantr	$⊢ (φ \land W \in (X L Y)) \to X \in P$
51	7	adantr	$⊢ (φ \land W \in (X L Y)) \to Y \in P$
52	9	adantr	$⊢ (φ \land W \in (X L Y)) \to X \neq Y$
53	1 2 3 49 50 51 52	tgelrnln	$⊢ (φ \land W \in (X L Y)) \to X L Y \in ran L$
54	28	adantr	$⊢ (φ \land W \in (X L Y)) \to Z \in P$
55	36	adantr	$⊢ (φ \land W \in (X L Y)) \to Z \neq Y$
56	1 2 3 49 54 51 55	tgelrnln	$⊢ (φ \land W \in (X L Y)) \to Z L Y \in ran L$
57	1 2 3 5 28 7 36	tglinerflx1	$⊢ φ \to Z \in (Z L Y)$
58	57	adantr	$⊢ (φ \land W \in (X L Y)) \to Z \in (Z L Y)$
59	8	eldifbd	$⊢ φ \to \neg Z \in (X L Y)$
60	59	adantr	$⊢ (φ \land W \in (X L Y)) \to \neg Z \in (X L Y)$
61		nelne1	$⊢ (Z \in (Z L Y) \land \neg Z \in (X L Y)) \to Z L Y \neq X L Y$
62	58 60 61	syl2anc	$⊢ (φ \land W \in (X L Y)) \to Z L Y \neq X L Y$
63	62	necomd	$⊢ (φ \land W \in (X L Y)) \to X L Y \neq Z L Y$
64	32	adantr	$⊢ (φ \land W \in (X L Y)) \to Y \in (X L Y)$
65	1 2 3 49 54 51 55	tglinerflx2	$⊢ (φ \land W \in (X L Y)) \to Y \in (Z L Y)$
66	64 65	elind	$⊢ (φ \land W \in (X L Y)) \to Y \in ((X L Y) \cap (Z L Y))$
67		simpr	$⊢ (φ \land W \in (X L Y)) \to W \in (X L Y)$
68	11	adantr	$⊢ (φ \land W \in (X L Y)) \to W \in P$
69	12	adantr	$⊢ (φ \land W \in (X L Y)) \to Y \in (Z I W)$
70	1 2 3 49 54 51 68 55 69	btwnlng3	$⊢ (φ \land W \in (X L Y)) \to W \in (Z L Y)$
71	67 70	elind	$⊢ (φ \land W \in (X L Y)) \to W \in ((X L Y) \cap (Z L Y))$
72	1 2 3 49 53 56 63 66 71	tglineineq	$⊢ (φ \land W \in (X L Y)) \to Y = W$
73	48 72	mtand	$⊢ φ \to \neg W \in (X L Y)$
74	73	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to \neg W \in (X L Y)$
75	39 74	eldifd	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to W \in (P ∖ (X L Y))$
76	9	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to X \neq Y$
77		eqid	$⊢ dist (G) = dist (G)$
78	1 77 2 5 28 7 11 12	tgbtwncom	$⊢ φ \to Y \in (W I Z)$
79	78	ad2antrr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Y \in (W I Z)$
80	37	necomd	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to Y \neq Z$
81	1 77 2 10 11 28 32 73 59 78	islnoppd	$⊢ φ \to W O Z$
82	81	ad3antrrr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to W O Z$
83	5	adantr	$⊢ (φ \land s \in ((X L Y) E Z)) \to G \in 𝒢_{Tarski}$
84	83	ad2antrr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to G \in 𝒢_{Tarski}$
85	31	adantr	$⊢ (φ \land s \in ((X L Y) E Z)) \to X \in P$
86	7	adantr	$⊢ (φ \land s \in ((X L Y) E Z)) \to Y \in P$
87	9	adantr	$⊢ (φ \land s \in ((X L Y) E Z)) \to X \neq Y$
88	1 2 3 83 85 86 87	tgelrnln	$⊢ (φ \land s \in ((X L Y) E Z)) \to X L Y \in ran L$
89	88	ad2antrr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to X L Y \in ran L$
90	8	adantr	$⊢ (φ \land s \in ((X L Y) E Z)) \to Z \in (P ∖ (X L Y))$
91	1 2 3 4 83 88 90 22	plngssp	$⊢ (φ \land s \in ((X L Y) E Z)) \to s \in P$
92	91	ad2antrr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to s \in P$
93	11	ad3antrrr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to W \in P$
94	28	ad3antrrr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to Z \in P$
95		simpr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to s O Z$
96	1 2 3 10 84 89 92 93 94 95	lnopp2hpgb	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to (W O Z \leftrightarrow s {hp}_{𝒢} (G) (X L Y) W)$
97	82 96	mpbid	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to s {hp}_{𝒢} (G) (X L Y) W$
98	97	orcd	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to (s {hp}_{𝒢} (G) (X L Y) W \lor s O W)$
99	98	ex	$⊢ ((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \to (s O Z \to (s {hp}_{𝒢} (G) (X L Y) W \lor s O W))$
100	99	ex	$⊢ (φ \land s \in ((X L Y) E Z)) \to (\neg s \in (X L Y) \to (s O Z \to (s {hp}_{𝒢} (G) (X L Y) W \lor s O W)))$
101	100	a2d	$⊢ (φ \land s \in ((X L Y) E Z)) \to ((\neg s \in (X L Y) \to s O Z) \to (\neg s \in (X L Y) \to (s {hp}_{𝒢} (G) (X L Y) W \lor s O W)))$
102		df-or	$⊢ (s \in (X L Y) \lor s O Z) \leftrightarrow (\neg s \in (X L Y) \to s O Z)$
103		df-or	$⊢ (s \in (X L Y) \lor (s {hp}_{𝒢} (G) (X L Y) W \lor s O W)) \leftrightarrow (\neg s \in (X L Y) \to (s {hp}_{𝒢} (G) (X L Y) W \lor s O W))$
104	101 102 103	3imtr4g	$⊢ (φ \land s \in ((X L Y) E Z)) \to ((s \in (X L Y) \lor s O Z) \to (s \in (X L Y) \lor (s {hp}_{𝒢} (G) (X L Y) W \lor s O W)))$
105	104	imp	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to (s \in (X L Y) \lor (s {hp}_{𝒢} (G) (X L Y) W \lor s O W))$
106		3orass	$⊢ (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W \lor s O W) \leftrightarrow (s \in (X L Y) \lor (s {hp}_{𝒢} (G) (X L Y) W \lor s O W))$
107	105 106	sylibr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W \lor s O W)$
108	88	adantr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to X L Y \in ran L$
109	91	adantr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to s \in P$
110	1 2 3 4 26 108 75 10 109	elplng	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to (s \in ((X L Y) E W) \leftrightarrow (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W \lor s O W))$
111	107 110	mpbird	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to s \in ((X L Y) E W)$
112	32	ad3antrrr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to Y \in (X L Y)$
113	59	ad3antrrr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to \neg Z \in (X L Y)$
114	73	ad3antrrr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to \neg W \in (X L Y)$
115	12	ad3antrrr	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to Y \in (Z I W)$
116	1 77 2 10 94 93 112 113 114 115	islnoppd	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to Z O W$
117	1 2 3 10 84 89 94 93 116	lnoppnhpg	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to \neg Z {hp}_{𝒢} (G) (X L Y) W$
118	89	adantr	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land W O s) \to X L Y \in ran L$
119	84	adantr	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land W O s) \to G \in 𝒢_{Tarski}$
120	93	adantr	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land W O s) \to W \in P$
121	92	adantr	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land W O s) \to s \in P$
122		simpr	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land W O s) \to W O s$
123	1 77 2 10 3 118 119 120 121 122	oppcom	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land W O s) \to s O W$
124	89	adantr	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land s O W) \to X L Y \in ran L$
125	84	adantr	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land s O W) \to G \in 𝒢_{Tarski}$
126	92	adantr	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land s O W) \to s \in P$
127	93	adantr	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land s O W) \to W \in P$
128		simpr	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land s O W) \to s O W$
129	1 77 2 10 3 124 125 126 127 128	oppcom	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \land s O W) \to W O s$
130	123 129	impbida	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to (W O s \leftrightarrow s O W)$
131	1 77 2 10 3 89 84 92 94 95	oppcom	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to Z O s$
132	1 2 3 10 84 89 94 93 92 131	lnopp2hpgb	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to (W O s \leftrightarrow Z {hp}_{𝒢} (G) (X L Y) W)$
133	130 132	bitr3d	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to (s O W \leftrightarrow Z {hp}_{𝒢} (G) (X L Y) W)$
134	117 133	mtbird	$⊢ (((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \land s O Z) \to \neg s O W$
135	134	ex	$⊢ ((φ \land s \in ((X L Y) E Z)) \land \neg s \in (X L Y)) \to (s O Z \to \neg s O W)$
136	135	ex	$⊢ (φ \land s \in ((X L Y) E Z)) \to (\neg s \in (X L Y) \to (s O Z \to \neg s O W))$
137	136	a2d	$⊢ (φ \land s \in ((X L Y) E Z)) \to ((\neg s \in (X L Y) \to s O Z) \to (\neg s \in (X L Y) \to \neg s O W))$
138	137	imp	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (\neg s \in (X L Y) \to s O Z)) \to (\neg s \in (X L Y) \to \neg s O W)$
139	102 138	sylan2b	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to (\neg s \in (X L Y) \to \neg s O W)$
140	139	imp	$⊢ (((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \land \neg s \in (X L Y)) \to \neg s O W$
141		df-3or	$⊢ (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W \lor s O W) \leftrightarrow ((s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W) \lor s O W)$
142		orcom	$⊢ ((s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W) \lor s O W) \leftrightarrow (s O W \lor (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W))$
143		df-or	$⊢ (s O W \lor (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W)) \leftrightarrow (\neg s O W \to (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W))$
144	141 142 143	3bitri	$⊢ (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W \lor s O W) \leftrightarrow (\neg s O W \to (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W))$
145	107 144	sylib	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to (\neg s O W \to (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W))$
146	145	imp	$⊢ (((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \land \neg s O W) \to (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W)$
147		df-or	$⊢ (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W) \leftrightarrow (\neg s \in (X L Y) \to s {hp}_{𝒢} (G) (X L Y) W)$
148	146 147	sylib	$⊢ (((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \land \neg s O W) \to (\neg s \in (X L Y) \to s {hp}_{𝒢} (G) (X L Y) W)$
149	148	imp	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \land \neg s O W) \land \neg s \in (X L Y)) \to s {hp}_{𝒢} (G) (X L Y) W$
150	149	an32s	$⊢ ((((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \land \neg s \in (X L Y)) \land \neg s O W) \to s {hp}_{𝒢} (G) (X L Y) W$
151	140 150	mpdan	$⊢ (((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \land \neg s \in (X L Y)) \to s {hp}_{𝒢} (G) (X L Y) W$
152	151	ex	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to (\neg s \in (X L Y) \to s {hp}_{𝒢} (G) (X L Y) W)$
153	152 147	sylibr	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) W)$
154	1 2 3 4 26 47 30 75 76 10 29 79 80 111 153	plngrotlem1	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to s \in ((W L Y) E X)$
155	45	eqcomd	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to W L Y = Z L Y$
156	155	oveq1d	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to (W L Y) E X = (Z L Y) E X$
157	154 156	eleqtrd	$⊢ ((φ \land s \in ((X L Y) E Z)) \land (s \in (X L Y) \lor s O Z)) \to s \in ((Z L Y) E X)$
158	1 2 3 4 83 88 90 10 91	elplng	$⊢ (φ \land s \in ((X L Y) E Z)) \to (s \in ((X L Y) E Z) \leftrightarrow (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z \lor s O Z))$
159	22 158	mpbid	$⊢ (φ \land s \in ((X L Y) E Z)) \to (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z \lor s O Z)$
160		3orass	$⊢ (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z \lor s O Z) \leftrightarrow (s \in (X L Y) \lor (s {hp}_{𝒢} (G) (X L Y) Z \lor s O Z))$
161		orordi	$⊢ (s \in (X L Y) \lor (s {hp}_{𝒢} (G) (X L Y) Z \lor s O Z)) \leftrightarrow ((s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z) \lor (s \in (X L Y) \lor s O Z))$
162	160 161	bitri	$⊢ (s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z \lor s O Z) \leftrightarrow ((s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z) \lor (s \in (X L Y) \lor s O Z))$
163	159 162	sylib	$⊢ (φ \land s \in ((X L Y) E Z)) \to ((s \in (X L Y) \lor s {hp}_{𝒢} (G) (X L Y) Z) \lor (s \in (X L Y) \lor s O Z))$
164	25 157 163	mpjaodan	$⊢ (φ \land s \in ((X L Y) E Z)) \to s \in ((Z L Y) E X)$
165	164	ex	$⊢ φ \to (s \in ((X L Y) E Z) \to s \in ((Z L Y) E X))$
166	165	ssrdv	$⊢ φ \to (X L Y) E Z \subseteq (Z L Y) E X$

Metamath Proof Explorer

Theorem plngrotlem2

Proof