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=ifA∈ωA∅→A+𝑜B=ifA∈ωA∅+𝑜B
2 1 1 oveq12d ⊢A=ifA∈ωA∅→A+𝑜B⋅𝑜A+𝑜B=ifA∈ωA∅+𝑜B⋅𝑜ifA∈ωA∅+𝑜B
3 2 oveq1d ⊢A=ifA∈ωA∅→A+𝑜B⋅𝑜A+𝑜B+𝑜B=ifA∈ωA∅+𝑜B⋅𝑜ifA∈ωA∅+𝑜B+𝑜B
4 3 eqeq1d ⊢A=ifA∈ωA∅→A+𝑜B⋅𝑜A+𝑜B+𝑜B=C+𝑜D⋅𝑜C+𝑜D+𝑜D↔ifA∈ωA∅+𝑜B⋅𝑜ifA∈ωA∅+𝑜B+𝑜B=C+𝑜D⋅𝑜C+𝑜D+𝑜D
5 eqeq1 ⊢A=ifA∈ωA∅→A=C↔ifA∈ωA∅=C
6 5 anbi1d ⊢A=ifA∈ωA∅→A=C∧B=D↔ifA∈ωA∅=C∧B=D
7 4 6 bibi12d ⊢A=ifA∈ωA∅→A+𝑜B⋅𝑜A+𝑜B+𝑜B=C+𝑜D⋅𝑜C+𝑜D+𝑜D↔A=C∧B=D↔ifA∈ωA∅+𝑜B⋅𝑜ifA∈ωA∅+𝑜B+𝑜B=C+𝑜D⋅𝑜C+𝑜D+𝑜D↔ifA∈ωA∅=C∧B=D
8 oveq2 ⊢B=ifB∈ωB∅→ifA∈ωA∅+𝑜B=ifA∈ωA∅+𝑜ifB∈ωB∅
9 8 8 oveq12d ⊢B=ifB∈ωB∅→ifA∈ωA∅+𝑜B⋅𝑜ifA∈ωA∅+𝑜B=ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅
10 id ⊢B=ifB∈ωB∅→B=ifB∈ωB∅
11 9 10 oveq12d ⊢B=ifB∈ωB∅→ifA∈ωA∅+𝑜B⋅𝑜ifA∈ωA∅+𝑜B+𝑜B=ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅
12 11 eqeq1d ⊢B=ifB∈ωB∅→ifA∈ωA∅+𝑜B⋅𝑜ifA∈ωA∅+𝑜B+𝑜B=C+𝑜D⋅𝑜C+𝑜D+𝑜D↔ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=C+𝑜D⋅𝑜C+𝑜D+𝑜D
13 eqeq1 ⊢B=ifB∈ωB∅→B=D↔ifB∈ωB∅=D
14 13 anbi2d ⊢B=ifB∈ωB∅→ifA∈ωA∅=C∧B=D↔ifA∈ωA∅=C∧ifB∈ωB∅=D
15 12 14 bibi12d ⊢B=ifB∈ωB∅→ifA∈ωA∅+𝑜B⋅𝑜ifA∈ωA∅+𝑜B+𝑜B=C+𝑜D⋅𝑜C+𝑜D+𝑜D↔ifA∈ωA∅=C∧B=D↔ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=C+𝑜D⋅𝑜C+𝑜D+𝑜D↔ifA∈ωA∅=C∧ifB∈ωB∅=D
16 oveq1 ⊢C=ifC∈ωC∅→C+𝑜D=ifC∈ωC∅+𝑜D
17 16 16 oveq12d ⊢C=ifC∈ωC∅→C+𝑜D⋅𝑜C+𝑜D=ifC∈ωC∅+𝑜D⋅𝑜ifC∈ωC∅+𝑜D
18 17 oveq1d ⊢C=ifC∈ωC∅→C+𝑜D⋅𝑜C+𝑜D+𝑜D=ifC∈ωC∅+𝑜D⋅𝑜ifC∈ωC∅+𝑜D+𝑜D
19 18 eqeq2d ⊢C=ifC∈ωC∅→ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=C+𝑜D⋅𝑜C+𝑜D+𝑜D↔ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=ifC∈ωC∅+𝑜D⋅𝑜ifC∈ωC∅+𝑜D+𝑜D
20 eqeq2 ⊢C=ifC∈ωC∅→ifA∈ωA∅=C↔ifA∈ωA∅=ifC∈ωC∅
21 20 anbi1d ⊢C=ifC∈ωC∅→ifA∈ωA∅=C∧ifB∈ωB∅=D↔ifA∈ωA∅=ifC∈ωC∅∧ifB∈ωB∅=D
22 19 21 bibi12d ⊢C=ifC∈ωC∅→ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=C+𝑜D⋅𝑜C+𝑜D+𝑜D↔ifA∈ωA∅=C∧ifB∈ωB∅=D↔ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=ifC∈ωC∅+𝑜D⋅𝑜ifC∈ωC∅+𝑜D+𝑜D↔ifA∈ωA∅=ifC∈ωC∅∧ifB∈ωB∅=D
23 oveq2 ⊢D=ifD∈ωD∅→ifC∈ωC∅+𝑜D=ifC∈ωC∅+𝑜ifD∈ωD∅
24 23 23 oveq12d ⊢D=ifD∈ωD∅→ifC∈ωC∅+𝑜D⋅𝑜ifC∈ωC∅+𝑜D=ifC∈ωC∅+𝑜ifD∈ωD∅⋅𝑜ifC∈ωC∅+𝑜ifD∈ωD∅
25 id ⊢D=ifD∈ωD∅→D=ifD∈ωD∅
26 24 25 oveq12d ⊢D=ifD∈ωD∅→ifC∈ωC∅+𝑜D⋅𝑜ifC∈ωC∅+𝑜D+𝑜D=ifC∈ωC∅+𝑜ifD∈ωD∅⋅𝑜ifC∈ωC∅+𝑜ifD∈ωD∅+𝑜ifD∈ωD∅
27 26 eqeq2d ⊢D=ifD∈ωD∅→ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=ifC∈ωC∅+𝑜D⋅𝑜ifC∈ωC∅+𝑜D+𝑜D↔ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=ifC∈ωC∅+𝑜ifD∈ωD∅⋅𝑜ifC∈ωC∅+𝑜ifD∈ωD∅+𝑜ifD∈ωD∅
28 eqeq2 ⊢D=ifD∈ωD∅→ifB∈ωB∅=D↔ifB∈ωB∅=ifD∈ωD∅
29 28 anbi2d ⊢D=ifD∈ωD∅→ifA∈ωA∅=ifC∈ωC∅∧ifB∈ωB∅=D↔ifA∈ωA∅=ifC∈ωC∅∧ifB∈ωB∅=ifD∈ωD∅
30 27 29 bibi12d ⊢D=ifD∈ωD∅→ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=ifC∈ωC∅+𝑜D⋅𝑜ifC∈ωC∅+𝑜D+𝑜D↔ifA∈ωA∅=ifC∈ωC∅∧ifB∈ωB∅=D↔ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=ifC∈ωC∅+𝑜ifD∈ωD∅⋅𝑜ifC∈ωC∅+𝑜ifD∈ωD∅+𝑜ifD∈ωD∅↔ifA∈ωA∅=ifC∈ωC∅∧ifB∈ωB∅=ifD∈ωD∅
31 peano1 ⊢∅∈ω
32 31 elimel ⊢ifA∈ωA∅∈ω
33 31 elimel ⊢ifB∈ωB∅∈ω
34 31 elimel ⊢ifC∈ωC∅∈ω
35 31 elimel ⊢ifD∈ωD∅∈ω
36 32 33 34 35 omopthi ⊢ifA∈ωA∅+𝑜ifB∈ωB∅⋅𝑜ifA∈ωA∅+𝑜ifB∈ωB∅+𝑜ifB∈ωB∅=ifC∈ωC∅+𝑜ifD∈ωD∅⋅𝑜ifC∈ωC∅+𝑜ifD∈ωD∅+𝑜ifD∈ωD∅↔ifA∈ωA∅=ifC∈ωC∅∧ifB∈ωB∅=ifD∈ω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