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	⊢ 𝐴 ∈ ω
	omopth.2	⊢ 𝐵 ∈ ω
	omopth.3	⊢ 𝐶 ∈ ω
	omopth.4	⊢ 𝐷 ∈ ω
Assertion	omopthi	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		omopth.1	⊢ 𝐴 ∈ ω
2		omopth.2	⊢ 𝐵 ∈ ω
3		omopth.3	⊢ 𝐶 ∈ ω
4		omopth.4	⊢ 𝐷 ∈ ω
5	1 2	nnacli	⊢ ( 𝐴 +o 𝐵 ) ∈ ω
6	5	nnoni	⊢ ( 𝐴 +o 𝐵 ) ∈ On
7	6	onordi	⊢ Ord ( 𝐴 +o 𝐵 )
8	3 4	nnacli	⊢ ( 𝐶 +o 𝐷 ) ∈ ω
9	8	nnoni	⊢ ( 𝐶 +o 𝐷 ) ∈ On
10	9	onordi	⊢ Ord ( 𝐶 +o 𝐷 )
11		ordtri3	⊢ ( ( Ord ( 𝐴 +o 𝐵 ) ∧ Ord ( 𝐶 +o 𝐷 ) ) → ( ( 𝐴 +o 𝐵 ) = ( 𝐶 +o 𝐷 ) ↔ ¬ ( ( 𝐴 +o 𝐵 ) ∈ ( 𝐶 +o 𝐷 ) ∨ ( 𝐶 +o 𝐷 ) ∈ ( 𝐴 +o 𝐵 ) ) ) )
12	7 10 11	mp2an	⊢ ( ( 𝐴 +o 𝐵 ) = ( 𝐶 +o 𝐷 ) ↔ ¬ ( ( 𝐴 +o 𝐵 ) ∈ ( 𝐶 +o 𝐷 ) ∨ ( 𝐶 +o 𝐷 ) ∈ ( 𝐴 +o 𝐵 ) ) )
13	12	con2bii	⊢ ( ( ( 𝐴 +o 𝐵 ) ∈ ( 𝐶 +o 𝐷 ) ∨ ( 𝐶 +o 𝐷 ) ∈ ( 𝐴 +o 𝐵 ) ) ↔ ¬ ( 𝐴 +o 𝐵 ) = ( 𝐶 +o 𝐷 ) )
14	1 2 8 4	omopthlem2	⊢ ( ( 𝐴 +o 𝐵 ) ∈ ( 𝐶 +o 𝐷 ) → ¬ ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) = ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) )
15		eqcom	⊢ ( ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) = ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) ↔ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) )
16	14 15	sylnib	⊢ ( ( 𝐴 +o 𝐵 ) ∈ ( 𝐶 +o 𝐷 ) → ¬ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) )
17	3 4 5 2	omopthlem2	⊢ ( ( 𝐶 +o 𝐷 ) ∈ ( 𝐴 +o 𝐵 ) → ¬ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) )
18	16 17	jaoi	⊢ ( ( ( 𝐴 +o 𝐵 ) ∈ ( 𝐶 +o 𝐷 ) ∨ ( 𝐶 +o 𝐷 ) ∈ ( 𝐴 +o 𝐵 ) ) → ¬ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) )
19	13 18	sylbir	⊢ ( ¬ ( 𝐴 +o 𝐵 ) = ( 𝐶 +o 𝐷 ) → ¬ ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) )
20	19	con4i	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → ( 𝐴 +o 𝐵 ) = ( 𝐶 +o 𝐷 ) )
21		id	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) )
22	20 20	oveq12d	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) = ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) )
23	22	oveq1d	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐷 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) )
24	21 23	eqtr4d	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐷 ) )
25	5 5	nnmcli	⊢ ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ∈ ω
26		nnacan	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐷 ∈ ω ) → ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐷 ) ↔ 𝐵 = 𝐷 ) )
27	25 2 4 26	mp3an	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐷 ) ↔ 𝐵 = 𝐷 )
28	24 27	sylib	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → 𝐵 = 𝐷 )
29	28	oveq2d	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → ( 𝐶 +o 𝐵 ) = ( 𝐶 +o 𝐷 ) )
30	20 29	eqtr4d	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → ( 𝐴 +o 𝐵 ) = ( 𝐶 +o 𝐵 ) )
31		nnacom	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) → ( 𝐵 +o 𝐴 ) = ( 𝐴 +o 𝐵 ) )
32	2 1 31	mp2an	⊢ ( 𝐵 +o 𝐴 ) = ( 𝐴 +o 𝐵 )
33		nnacom	⊢ ( ( 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐵 +o 𝐶 ) = ( 𝐶 +o 𝐵 ) )
34	2 3 33	mp2an	⊢ ( 𝐵 +o 𝐶 ) = ( 𝐶 +o 𝐵 )
35	30 32 34	3eqtr4g	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → ( 𝐵 +o 𝐴 ) = ( 𝐵 +o 𝐶 ) )
36		nnacan	⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐵 +o 𝐴 ) = ( 𝐵 +o 𝐶 ) ↔ 𝐴 = 𝐶 ) )
37	2 1 3 36	mp3an	⊢ ( ( 𝐵 +o 𝐴 ) = ( 𝐵 +o 𝐶 ) ↔ 𝐴 = 𝐶 )
38	35 37	sylib	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → 𝐴 = 𝐶 )
39	38 28	jca	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )
40		oveq12	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( 𝐴 +o 𝐵 ) = ( 𝐶 +o 𝐷 ) )
41	40 40	oveq12d	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) = ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) )
42		simpr	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → 𝐵 = 𝐷 )
43	41 42	oveq12d	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) )
44	39 43	impbii	⊢ ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )