This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )