Theorem omopthi

Description: An ordered pair theorem for _om . Theorem 17.3 of Quine p. 124. This proof is adapted from nn0opthi . (Contributed by Scott Fenton, 16-Apr-2012) (Revised by Mario Carneiro, 17-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		omopth.1	$$⊢A\in \mathrm{\omega }$$
2		omopth.2	$$⊢B\in \mathrm{\omega }$$
3		omopth.3	$$⊢C\in \mathrm{\omega }$$
4		omopth.4	$$⊢D\in \mathrm{\omega }$$
5	1 2	nnacli	$$⊢A{+}_{𝑜}B\in \mathrm{\omega }$$
6	5	nnoni	$$⊢A{+}_{𝑜}B\in \mathrm{On}$$
7	6	onordi	$$⊢\mathrm{Ord}\left(A{+}_{𝑜}B\right)$$
8	3 4	nnacli	$$⊢C{+}_{𝑜}D\in \mathrm{\omega }$$
9	8	nnoni	$$⊢C{+}_{𝑜}D\in \mathrm{On}$$
10	9	onordi	$$⊢\mathrm{Ord}\left(C{+}_{𝑜}D\right)$$
11		ordtri3	$$⊢\left(\mathrm{Ord}\left(A{+}_{𝑜}B\right)\wedge \mathrm{Ord}\left(C{+}_{𝑜}D\right)\right)\to \left(A{+}_{𝑜}B=C{+}_{𝑜}D\leftrightarrow \neg \left(A{+}_{𝑜}B\in \left(C{+}_{𝑜}D\right)\vee C{+}_{𝑜}D\in \left(A{+}_{𝑜}B\right)\right)\right)$$
12	7 10 11	mp2an	$$⊢A{+}_{𝑜}B=C{+}_{𝑜}D\leftrightarrow \neg \left(A{+}_{𝑜}B\in \left(C{+}_{𝑜}D\right)\vee C{+}_{𝑜}D\in \left(A{+}_{𝑜}B\right)\right)$$
13	12	con2bii	$$⊢\left(A{+}_{𝑜}B\in \left(C{+}_{𝑜}D\right)\vee C{+}_{𝑜}D\in \left(A{+}_{𝑜}B\right)\right)\leftrightarrow \neg A{+}_{𝑜}B=C{+}_{𝑜}D$$
14	1 2 8 4	omopthlem2	$$⊢A{+}_{𝑜}B\in \left(C{+}_{𝑜}D\right)\to \neg \left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B$$
15		eqcom	$$⊢\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B\leftrightarrow \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D$$
16	14 15	sylnib	$$⊢A{+}_{𝑜}B\in \left(C{+}_{𝑜}D\right)\to \neg \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D$$
17	3 4 5 2	omopthlem2	$$⊢C{+}_{𝑜}D\in \left(A{+}_{𝑜}B\right)\to \neg \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D$$
18	16 17	jaoi	$$⊢\left(A{+}_{𝑜}B\in \left(C{+}_{𝑜}D\right)\vee C{+}_{𝑜}D\in \left(A{+}_{𝑜}B\right)\right)\to \neg \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D$$
19	13 18	sylbir	$$⊢\neg A{+}_{𝑜}B=C{+}_{𝑜}D\to \neg \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D$$
20	19	con4i	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to A{+}_{𝑜}B=C{+}_{𝑜}D$$
21		id	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D$$
22	20 20	oveq12d	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to \left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)=\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)$$
23	22	oveq1d	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}D=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D$$
24	21 23	eqtr4d	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}D$$
25	5 5	nnmcli	$$⊢\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\in \mathrm{\omega }$$
26		nnacan	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\in \mathrm{\omega }\wedge B\in \mathrm{\omega }\wedge D\in \mathrm{\omega }\right)\to \left(\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}D\leftrightarrow B=D\right)$$
27	25 2 4 26	mp3an	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}D\leftrightarrow B=D$$
28	24 27	sylib	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to B=D$$
29	28	oveq2d	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to C{+}_{𝑜}B=C{+}_{𝑜}D$$
30	20 29	eqtr4d	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to A{+}_{𝑜}B=C{+}_{𝑜}B$$
31		nnacom	$$⊢\left(B\in \mathrm{\omega }\wedge A\in \mathrm{\omega }\right)\to B{+}_{𝑜}A=A{+}_{𝑜}B$$
32	2 1 31	mp2an	$$⊢B{+}_{𝑜}A=A{+}_{𝑜}B$$
33		nnacom	$$⊢\left(B\in \mathrm{\omega }\wedge C\in \mathrm{\omega }\right)\to B{+}_{𝑜}C=C{+}_{𝑜}B$$
34	2 3 33	mp2an	$$⊢B{+}_{𝑜}C=C{+}_{𝑜}B$$
35	30 32 34	3eqtr4g	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to B{+}_{𝑜}A=B{+}_{𝑜}C$$
36		nnacan	$$⊢\left(B\in \mathrm{\omega }\wedge A\in \mathrm{\omega }\wedge C\in \mathrm{\omega }\right)\to \left(B{+}_{𝑜}A=B{+}_{𝑜}C\leftrightarrow A=C\right)$$
37	2 1 3 36	mp3an	$$⊢B{+}_{𝑜}A=B{+}_{𝑜}C\leftrightarrow A=C$$
38	35 37	sylib	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to A=C$$
39	38 28	jca	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\to \left(A=C\wedge B=D\right)$$
40		oveq12	$$⊢\left(A=C\wedge B=D\right)\to A{+}_{𝑜}B=C{+}_{𝑜}D$$
41	40 40	oveq12d	$$⊢\left(A=C\wedge B=D\right)\to \left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)=\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)$$
42		simpr	$$⊢\left(A=C\wedge B=D\right)\to B=D$$
43	41 42	oveq12d	$$⊢\left(A=C\wedge B=D\right)\to \left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D$$
44	39 43	impbii	$$⊢\left(\left(A{+}_{𝑜}B\right){\cdot }_{𝑜}\left(A{+}_{𝑜}B\right)\right){+}_{𝑜}B=\left(\left(C{+}_{𝑜}D\right){\cdot }_{𝑜}\left(C{+}_{𝑜}D\right)\right){+}_{𝑜}D\leftrightarrow \left(A=C\wedge B=D\right)$$