Metamath Proof Explorer

Theorem omopth

Description: An ordered pair theorem for finite integers. Analogous to nn0opthi . (Contributed by Scott Fenton, 1-May-2012)

Ref Expression
Assertion omopth ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐶 ∈ ω ∧ 𝐷 ∈ ω ) ) → ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → ( 𝐴 +o 𝐵 ) = ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) )
2 1 1 oveq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) = ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ) )
3 2 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ) +o 𝐵 ) )
4 3 eqeq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ) )
5 eqeq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → ( 𝐴 = 𝐶 ↔ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = 𝐶 ) )
6 5 anbi1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
7 4 6 bibi12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ω , 𝐴 , ∅ ) → ( ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ↔ ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
8 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) = ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) )
9 8 8 oveq12d ⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ) = ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) )
10 id ⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) )
11 9 10 oveq12d ⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ) +o 𝐵 ) = ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) )
12 11 eqeq1d ⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ) )
13 eqeq1 ⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → ( 𝐵 = 𝐷 ↔ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = 𝐷 ) )
14 13 anbi2d ⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = 𝐶 ∧ 𝐵 = 𝐷 ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = 𝐶 ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = 𝐷 ) ) )
15 12 14 bibi12d ⊢ ( 𝐵 = if ( 𝐵 ∈ ω , 𝐵 , ∅ ) → ( ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = 𝐶 ∧ 𝐵 = 𝐷 ) ) ↔ ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = 𝐶 ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = 𝐷 ) ) ) )
16 oveq1 ⊢ ( 𝐶 = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) → ( 𝐶 +o 𝐷 ) = ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) )
17 16 16 oveq12d ⊢ ( 𝐶 = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) → ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) = ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ) )
18 17 oveq1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) → ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) = ( ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ) +o 𝐷 ) )
19 18 eqeq2d ⊢ ( 𝐶 = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) → ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ) +o 𝐷 ) ) )
20 eqeq2 ⊢ ( 𝐶 = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) → ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = 𝐶 ↔ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) ) )
21 20 anbi1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) → ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = 𝐶 ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = 𝐷 ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = 𝐷 ) ) )
22 19 21 bibi12d ⊢ ( 𝐶 = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) → ( ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = 𝐶 ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = 𝐷 ) ) ↔ ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ) +o 𝐷 ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = 𝐷 ) ) ) )
23 oveq2 ⊢ ( 𝐷 = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) → ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) = ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) )
24 23 23 oveq12d ⊢ ( 𝐷 = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) → ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ) = ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ) )
25 id ⊢ ( 𝐷 = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) → 𝐷 = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) )
26 24 25 oveq12d ⊢ ( 𝐷 = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) → ( ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ) +o 𝐷 ) = ( ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) )
27 26 eqeq2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) → ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ) +o 𝐷 ) ↔ ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ) )
28 eqeq2 ⊢ ( 𝐷 = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) → ( if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = 𝐷 ↔ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) )
29 28 anbi2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) → ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = 𝐷 ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ) )
30 27 29 bibi12d ⊢ ( 𝐷 = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) → ( ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o 𝐷 ) ) +o 𝐷 ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = 𝐷 ) ) ↔ ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ) ) )
31 peano1 ⊢ ∅ ∈ ω
32 31 elimel ⊢ if ( 𝐴 ∈ ω , 𝐴 , ∅ ) ∈ ω
33 31 elimel ⊢ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ∈ ω
34 31 elimel ⊢ if ( 𝐶 ∈ ω , 𝐶 , ∅ ) ∈ ω
35 31 elimel ⊢ if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ∈ ω
36 32 33 34 35 omopthi ⊢ ( ( ( ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ·o ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) ) +o if ( 𝐵 ∈ ω , 𝐵 , ∅ ) ) = ( ( ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ·o ( if ( 𝐶 ∈ ω , 𝐶 , ∅ ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ) +o if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) ↔ ( if ( 𝐴 ∈ ω , 𝐴 , ∅ ) = if ( 𝐶 ∈ ω , 𝐶 , ∅ ) ∧ if ( 𝐵 ∈ ω , 𝐵 , ∅ ) = if ( 𝐷 ∈ ω , 𝐷 , ∅ ) ) )
37 7 15 22 30 36 dedth4h ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐶 ∈ ω ∧ 𝐷 ∈ ω ) ) → ( ( ( ( 𝐴 +o 𝐵 ) ·o ( 𝐴 +o 𝐵 ) ) +o 𝐵 ) = ( ( ( 𝐶 +o 𝐷 ) ·o ( 𝐶 +o 𝐷 ) ) +o 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )