Theorem omopthlem2

Description: Lemma for omopthi . (Contributed by Scott Fenton, 16-Apr-2012) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Hypotheses	omopthlem2.1	$$⊢A\in \mathrm{\omega }$$
	omopthlem2.2	$$⊢B\in \mathrm{\omega }$$
	omopthlem2.3	$$⊢C\in \mathrm{\omega }$$
	omopthlem2.4	$$⊢D\in \mathrm{\omega }$$
Assertion	omopthlem2	$$⊢A{+}_{𝑜}B\in C\to \neg \left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B$$

Proof

Step	Hyp	Ref	Expression
1		omopthlem2.1	$$⊢A\in \mathrm{\omega }$$
2		omopthlem2.2	$$⊢B\in \mathrm{\omega }$$
3		omopthlem2.3	$$⊢C\in \mathrm{\omega }$$
4		omopthlem2.4	$$⊢D\in \mathrm{\omega }$$
5	3 3	nnmcli	$$⊢C{\cdot }_{𝑜}C\in \mathrm{\omega }$$
6	5 4	nnacli	$$⊢\left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D\in \mathrm{\omega }$$
7	6	nnoni	$$⊢\left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D\in \mathrm{On}$$
8	7	onirri	$$⊢\neg \left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D\in \left(\left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D\right)$$
9		eleq1	$$⊢\left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\to \left(\left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D\in \left(\left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D\right)\leftrightarrow \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\in \left(\left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D\right)\right)$$
10	8 9	mtbii	$$⊢\left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\to \neg \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\in \left(\left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D\right)$$
11		nnaword1	$$⊢\left(C{\cdot }_{𝑜}C\in \mathrm{\omega }\wedge D\in \mathrm{\omega }\right)\to C{\cdot }_{𝑜}C\subseteq \left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D$$
12	5 4 11	mp2an	$$⊢C{\cdot }_{𝑜}C\subseteq \left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D$$
13	1 2	nnacli	$$⊢A{+}_{𝑜}B\in \mathrm{\omega }$$
14	13 1	nnacli	$$⊢\left(A{+}_{𝑜}B\right){+}_{𝑜}A\in \mathrm{\omega }$$
15		nnaword1	$$⊢\left(B\in \mathrm{\omega }\wedge \left(A{+}_{𝑜}B\right){+}_{𝑜}A\in \mathrm{\omega }\right)\to B\subseteq B{+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}A\right)$$
16	2 14 15	mp2an	$$⊢B\subseteq B{+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}A\right)$$
17		nnacom	$$⊢\left(B\in \mathrm{\omega }\wedge \left(A{+}_{𝑜}B\right){+}_{𝑜}A\in \mathrm{\omega }\right)\to B{+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}A\right)=\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}A\right){+}_{𝑜}B$$
18	2 14 17	mp2an	$$⊢B{+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}A\right)=\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}A\right){+}_{𝑜}B$$
19	16 18	sseqtri	$$⊢B\subseteq \left(\left(A{+}_{𝑜}B\right){+}_{𝑜}A\right){+}_{𝑜}B$$
20		nnaass	$$⊢\left(A{+}_{𝑜}B\in \mathrm{\omega }\wedge A\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(\left(A{+}_{𝑜}B\right){+}_{𝑜}A\right){+}_{𝑜}B=\left(A{+}_{𝑜}B\right){+}_{𝑜}\left(A{+}_{𝑜}B\right)$$
21	13 1 2 20	mp3an	$$⊢\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}A\right){+}_{𝑜}B=\left(A{+}_{𝑜}B\right){+}_{𝑜}\left(A{+}_{𝑜}B\right)$$
22		nnm2	$$⊢A{+}_{𝑜}B\in \mathrm{\omega }\to \left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}=\left(A{+}_{𝑜}B\right){+}_{𝑜}\left(A{+}_{𝑜}B\right)$$
23	13 22	ax-mp	$$⊢\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}=\left(A{+}_{𝑜}B\right){+}_{𝑜}\left(A{+}_{𝑜}B\right)$$
24	21 23	eqtr4i	$$⊢\left(\left(A{+}_{𝑜}B\right){+}_{𝑜}A\right){+}_{𝑜}B=\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}$$
25	19 24	sseqtri	$$⊢B\subseteq \left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}$$
26		2onn	$$⊢2_{𝑜}\in \mathrm{\omega }$$
27	13 26	nnmcli	$$⊢\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\in \mathrm{\omega }$$
28	13 13	nnmcli	$$⊢\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\in \mathrm{\omega }$$
29		nnawordi	$$⊢\left(B\in \mathrm{\omega }\wedge \left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\in \mathrm{\omega }\wedge \left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\in \mathrm{\omega }\right)\to \left(B\subseteq \left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\to B{+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right)\subseteq \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right)\right)$$
30	2 27 28 29	mp3an	$$⊢B\subseteq \left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\to B{+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right)\subseteq \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right)$$
31	25 30	ax-mp	$$⊢B{+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right)\subseteq \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right)$$
32		nnacom	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\right)\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=B{+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right)$$
33	28 2 32	mp2an	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=B{+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right)$$
34		nnacom	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\in \mathrm{\omega }\wedge \left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\in \mathrm{\omega }\right)\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right)=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right)$$
35	28 27 34	mp2an	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right)=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right)$$
36	31 33 35	3sstr4i	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\subseteq \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right)$$
37	13 3	omopthlem1	$$⊢A{+}_{𝑜}B\in C\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right)\in \left(C{\cdot }_{𝑜}C\right)$$
38	28 2	nnacli	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\in \mathrm{\omega }$$
39	38	nnoni	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\in \mathrm{On}$$
40	5	nnoni	$$⊢C{\cdot }_{𝑜}C\in \mathrm{On}$$
41		ontr2	$$⊢\left(\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\in \mathrm{On}\wedge C{\cdot }_{𝑜}C\in \mathrm{On}\right)\to \left(\left(\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\subseteq \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right)\wedge \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right)\in \left(C{\cdot }_{𝑜}C\right)\right)\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\in \left(C{\cdot }_{𝑜}C\right)\right)$$
42	39 40 41	mp2an	$$⊢\left(\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\subseteq \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right)\wedge \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}{2}_{𝑜}\right)\in \left(C{\cdot }_{𝑜}C\right)\right)\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\in \left(C{\cdot }_{𝑜}C\right)$$
43	36 37 42	sylancr	$$⊢A{+}_{𝑜}B\in C\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\in \left(C{\cdot }_{𝑜}C\right)$$
44	12 43	sselid	$$⊢A{+}_{𝑜}B\in C\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\in \left(\left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D\right)$$
45	10 44	nsyl3	$$⊢A{+}_{𝑜}B\in C\to \neg \left(C{\cdot }_{𝑜}C\right){+}_{𝑜}D=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B$$