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 ⊢ A ∈ ω ∧ B ∈ ω ∧ C ∈ ω ∧ D ∈ ω → A + 𝑜 B ⋅ 𝑜 A + 𝑜 B + 𝑜 B = C + 𝑜 D ⋅ 𝑜 C + 𝑜 D + 𝑜 D ↔ A = C ∧ B = D

Proof

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